Metamath Proof Explorer


Syntax definition czs12

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

Ref Expression
Assertion czs12 class s[1/2]