Metamath Proof Explorer

Table of Contents - 5.2.2. Infinity and the extended real number system

1. cpnf
2. cmnf
3. cxr
4. clt
5. cle
6. df-pnf
7. df-mnf
8. df-xr
9. df-ltxr
10. df-le
11. pnfnre
12. pnfnre2
13. mnfnre
14. ressxr
15. rexpssxrxp
16. rexr
17. 0xr
18. renepnf
19. renemnf
20. rexrd
21. renepnfd
22. renemnfd
23. pnfex
24. pnfxr
25. pnfnemnf
26. mnfnepnf
27. mnfxr
28. rexri
29. 1xr
30. renfdisj
31. ltrelxr
32. ltrel
33. lerelxr
34. lerel
35. xrlenlt
36. xrlenltd
37. xrltnle
38. xrnltled
39. ssxr
40. ltxrlt