Metamath Proof Explorer


Syntax definition cz12s

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

Ref Expression
Assertion cz12s class s[1/2]