Database
SURREAL NUMBERS
Subsystems of surreals
Dyadic fractions
czs12
Next ⟩
df-zs12
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
czs12
Description:
Define the syntax for the set of surreal dyadic fractions.
Ref
Expression
Assertion
czs12
Could not format assertion : No typesetting found for class ZZ_s[1/2] with typecode class