Database
SURREAL NUMBERS
Subsystems of surreals
Dyadic fractions
cz12s
Next ⟩
df-z12s
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cz12s
Description:
Define the syntax for the set of surreal dyadic fractions.
Ref
Expression
Assertion
cz12s
class ZZ_s[1/2]