Metamath Proof Explorer

Table of Contents - 9. BASIC ORDER THEORY

1. Dual of an order structure
   1. codu
   2. df-odu
   3. oduval
   4. oduleval
   5. oduleg
   6. odubas
   7. odubasOLD
2. Preordered sets and directed sets
   1. cproset
   2. cdrs
   3. df-proset
   4. df-drs
   5. isprs
   6. prslem
   7. prsref
   8. prstr
   9. isdrs
   10. drsdir
   11. drsprs
   12. drsbn0
   13. drsdirfi
   14. isdrs2
3. Partially ordered sets (posets)
   1. cpo
   2. cplt
   3. club
   4. cglb
   5. cjn
   6. cmee
   7. df-poset
   8. ispos
   9. ispos2
   10. posprs
   11. posi
   12. posref
   13. posasymb
   14. postr
   15. 0pos
   16. 0posOLD
   17. isposd
   18. isposi
   19. isposix
   20. isposixOLD
   21. pospropd
   22. odupos
   23. oduposb
   24. df-plt
   25. pltfval
   26. pltval
   27. pltle
   28. pltne
   29. pltirr
   30. pleval2i
   31. pleval2
   32. pltnle
   33. pltval3
   34. pltnlt
   35. pltn2lp
   36. plttr
   37. pltletr
   38. plelttr
   39. pospo
   40. df-lub
   41. df-glb
   42. df-join
   43. df-meet
   44. lubfval
   45. lubdm
   46. lubfun
   47. lubeldm
   48. lubelss
   49. lubeu
   50. lubval
   51. lubcl
   52. lubprop
   53. luble
   54. lublecllem
   55. lublecl
   56. lubid
   57. glbfval
   58. glbdm
   59. glbfun
   60. glbeldm
   61. glbelss
   62. glbeu
   63. glbval
   64. glbcl
   65. glbprop
   66. glble
   67. joinfval
   68. joinfval2
   69. joindm
   70. joindef
   71. joinval
   72. joincl
   73. joindmss
   74. joinval2lem
   75. joinval2
   76. joineu
   77. joinlem
   78. lejoin1
   79. lejoin2
   80. joinle
   81. meetfval
   82. meetfval2
   83. meetdm
   84. meetdef
   85. meetval
   86. meetcl
   87. meetdmss
   88. meetval2lem
   89. meetval2
   90. meeteu
   91. meetlem
   92. lemeet1
   93. lemeet2
   94. meetle
   95. joincomALT
   96. joincom
   97. meetcomALT
   98. meetcom
   99. join0
   100. meet0
   101. odulub
   102. odujoin
   103. oduglb
   104. odumeet
   105. poslubmo
   106. posglbmo
   107. poslubd
   108. poslubdg
   109. posglbdg
4. Totally ordered sets (tosets)
   1. ctos
   2. df-toset
   3. istos
   4. tosso
   5. tospos
   6. tleile
   7. tltnle
   8. cp0
   9. cp1
   10. df-p0
   11. df-p1
   12. p0val
   13. p1val
   14. p0le
   15. ple1
5. Lattices
   1. Lattices
   2. Complete lattices
   3. Distributive lattices
   4. Subset order structures
6. Posets, directed sets, and lattices as relations
   1. Posets and lattices as relations
   2. Directed sets, nets