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. xrsupssd
30. infxrcl
31. infxrlb
32. infxrgelb
33. infxrre
34. infxrmnf
35. xrinf0
36. infxrss
37. reltre
38. rpltrp
39. reltxrnmnf
40. infmremnf
41. infmrp1