Metamath Proof Explorer
Table of Contents - 5.2.2. Infinity and the extended real number system
- cpnf
- cmnf
- cxr
- clt
- cle
- df-pnf
- df-mnf
- df-xr
- df-ltxr
- df-le
- pnfnre
- pnfnre2
- mnfnre
- ressxr
- rexpssxrxp
- rexr
- 0xr
- renepnf
- renemnf
- rexrd
- renepnfd
- renemnfd
- pnfex
- pnfxr
- pnfnemnf
- mnfnepnf
- mnfxr
- rexri
- 1xr
- renfdisj
- ltrelxr
- ltrel
- lerelxr
- lerel
- xrlenlt
- xrlenltd
- xrltnle
- xrnltled
- ssxr
- ltxrlt