Metamath Proof Explorer

Syntax definition cxrh

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

Ref Expression
Assertion cxrh 
class RR*Hom