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
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. oduprs
   10. isdrs
   11. drsdir
   12. drsprs
   13. drsbn0
   14. drsdirfi
   15. 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. isposd
   17. isposi
   18. isposix
   19. pospropd
   20. odupos
   21. oduposb
   22. df-plt
   23. pltfval
   24. pltval
   25. pltle
   26. pltne
   27. pltirr
   28. pleval2i
   29. pleval2
   30. pltnle
   31. pltval3
   32. pltnlt
   33. pltn2lp
   34. plttr
   35. pltletr
   36. plelttr
   37. pospo
   38. df-lub
   39. df-glb
   40. df-join
   41. df-meet
   42. lubfval
   43. lubdm
   44. lubfun
   45. lubeldm
   46. lubelss
   47. lubeu
   48. lubval
   49. lubcl
   50. lubprop
   51. luble
   52. lublecllem
   53. lublecl
   54. lubid
   55. glbfval
   56. glbdm
   57. glbfun
   58. glbeldm
   59. glbelss
   60. glbeu
   61. glbval
   62. glbcl
   63. glbprop
   64. glble
   65. joinfval
   66. joinfval2
   67. joindm
   68. joindef
   69. joinval
   70. joincl
   71. joindmss
   72. joinval2lem
   73. joinval2
   74. joineu
   75. joinlem
   76. lejoin1
   77. lejoin2
   78. joinle
   79. meetfval
   80. meetfval2
   81. meetdm
   82. meetdef
   83. meetval
   84. meetcl
   85. meetdmss
   86. meetval2lem
   87. meetval2
   88. meeteu
   89. meetlem
   90. lemeet1
   91. lemeet2
   92. meetle
   93. joincomALT
   94. joincom
   95. meetcomALT
   96. meetcom
   97. join0
   98. meet0
   99. odulub
   100. odujoin
   101. oduglb
   102. odumeet
   103. poslubmo
   104. posglbmo
   105. poslubd
   106. poslubdg
   107. 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