Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Natural operations on ordinals
cnadd
Next ⟩
df-nadd
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cnadd
Description:
Declare the syntax for natural ordinal addition. See
df-nadd
.
Ref
Expression
Assertion
cnadd
class
+no