Metamath Proof Explorer

Table of Contents - 2.4.38. Supremum and infimum

1. csup
2. cinf
3. df-sup
4. df-inf
5. dfsup2
6. supeq1
7. supeq1d
8. supeq1i
9. supeq2
10. supeq3
11. supeq123d
12. nfsup
13. supmo
14. supexd
15. supeu
16. supval2
17. eqsup
18. eqsupd
19. supcl
20. supub
21. suplub
22. suplub2
23. supnub
24. supssd
25. supex
26. sup00
27. sup0riota
28. sup0
29. supmax
30. fisup2g
31. fisupcl
32. supgtoreq
33. suppr
34. supsn
35. supisolem
36. supisoex
37. supiso
38. infeq1
39. infeq1d
40. infeq1i
41. infeq2
42. infeq3
43. infeq123d
44. nfinf
45. infexd
46. eqinf
47. eqinfd
48. infval
49. infcllem
50. infcl
51. inflb
52. infglb
53. infglbb
54. infnlb
55. infssd
56. infex
57. infmin
58. infmo
59. infeu
60. fimin2g
61. fiming
62. fiinfg
63. fiinf2g
64. fiinfcl
65. infltoreq
66. infpr
67. infsupprpr
68. infsn
69. inf00
70. infempty
71. infiso