Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal Numbers
cbday
Next ⟩
df-no
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cbday
Description:
Declare the birthday function for surreal numbers (see
df-bday
).
Ref
Expression
Assertion
cbday
class
bday