Metamath Proof Explorer


Syntax definition cer

Description: Equivalence class used to construct signed reals.

Ref Expression
Assertion cer class ~ 𝑹