Metamath Proof Explorer

Table of Contents - 9.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