Metamath Proof Explorer


Syntax definition cz12s

Description: Define the syntax for the set of surreal dyadic fractions.

Ref Expression
Assertion cz12s
class ZZ_s[1/2]