Metamath Proof Explorer

Table of Contents - 5.5.3. Supremum and infimum on the extended reals

1. xrsupexmnf
2. xrinfmexpnf
3. xrsupsslem
4. xrinfmsslem
5. xrsupss
6. xrinfmss
7. xrinfmss2
8. xrub
9. supxr
10. supxr2
11. supxrcl
12. supxrun
13. supxrmnf
14. supxrpnf
15. supxrunb1
16. supxrunb2
17. supxrbnd1
18. supxrbnd2
19. xrsup0
20. supxrub
21. supxrlub
22. supxrleub
23. supxrre
24. supxrbnd
25. supxrgtmnf
26. supxrre1
27. supxrre2
28. supxrss
29. infxrcl
30. infxrlb
31. infxrgelb
32. infxrre
33. infxrmnf
34. xrinf0
35. infxrss
36. reltre
37. rpltrp
38. reltxrnmnf
39. infmremnf
40. infmrp1