Metamath Proof Explorer


Syntax definition cxrh

Description: Map the extended real numbers into a complete lattice.

Ref Expression
Assertion cxrh class *Hom