Metamath Proof Explorer

Table of Contents - 9.2. Posets and lattices using extensible structures

1. 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. df-plt
   20. pltfval
   21. pltval
   22. pltle
   23. pltne
   24. pltirr
   25. pleval2i
   26. pleval2
   27. pltnle
   28. pltval3
   29. pltnlt
   30. pltn2lp
   31. plttr
   32. pltletr
   33. plelttr
   34. pospo
   35. df-lub
   36. df-glb
   37. df-join
   38. df-meet
   39. lubfval
   40. lubdm
   41. lubfun
   42. lubeldm
   43. lubelss
   44. lubeu
   45. lubval
   46. lubcl
   47. lubprop
   48. luble
   49. lublecllem
   50. lublecl
   51. lubid
   52. glbfval
   53. glbdm
   54. glbfun
   55. glbeldm
   56. glbelss
   57. glbeu
   58. glbval
   59. glbcl
   60. glbprop
   61. glble
   62. joinfval
   63. joinfval2
   64. joindm
   65. joindef
   66. joinval
   67. joincl
   68. joindmss
   69. joinval2lem
   70. joinval2
   71. joineu
   72. joinlem
   73. lejoin1
   74. lejoin2
   75. joinle
   76. meetfval
   77. meetfval2
   78. meetdm
   79. meetdef
   80. meetval
   81. meetcl
   82. meetdmss
   83. meetval2lem
   84. meetval2
   85. meeteu
   86. meetlem
   87. lemeet1
   88. lemeet2
   89. meetle
   90. joincomALT
   91. joincom
   92. meetcomALT
   93. meetcom
   94. ctos
   95. df-toset
   96. istos
   97. tosso
   98. cp0
   99. cp1
   100. df-p0
   101. df-p1
   102. p0val
   103. p1val
   104. p0le
   105. ple1
2. Lattices
   1. clat
   2. df-lat
   3. islat
   4. latcl2
   5. latlem
   6. latpos
   7. latjcl
   8. latmcl
   9. latref
   10. latasymb
   11. latasym
   12. lattr
   13. latasymd
   14. lattrd
   15. latjcom
   16. latlej1
   17. latlej2
   18. latjle12
   19. latleeqj1
   20. latleeqj2
   21. latjlej1
   22. latjlej2
   23. latjlej12
   24. latnlej
   25. latnlej1l
   26. latnlej1r
   27. latnlej2
   28. latnlej2l
   29. latnlej2r
   30. latjidm
   31. latmcom
   32. latmle1
   33. latmle2
   34. latlem12
   35. latleeqm1
   36. latleeqm2
   37. latmlem1
   38. latmlem2
   39. latmlem12
   40. latnlemlt
   41. latnle
   42. latmidm
   43. latabs1
   44. latabs2
   45. latledi
   46. latmlej11
   47. latmlej12
   48. latmlej21
   49. latmlej22
   50. lubsn
   51. latjass
   52. latj12
   53. latj32
   54. latj13
   55. latj31
   56. latjrot
   57. latj4
   58. latj4rot
   59. latjjdi
   60. latjjdir
   61. mod1ile
   62. mod2ile
   63. ccla
   64. df-clat
   65. isclat
   66. clatpos
   67. clatlem
   68. clatlubcl
   69. clatlubcl2
   70. clatglbcl
   71. clatglbcl2
   72. clatl
   73. isglbd
   74. lublem
   75. lubub
   76. lubl
   77. lubss
   78. lubel
   79. lubun
   80. clatglb
   81. clatglble
   82. clatleglb
   83. clatglbss
3. The dual of an ordered set
   1. codu
   2. df-odu
   3. oduval
   4. oduleval
   5. oduleg
   6. odubas
   7. pospropd
   8. odupos
   9. oduposb
   10. meet0
   11. join0
   12. oduglb
   13. odumeet
   14. odulub
   15. odujoin
   16. odulatb
   17. oduclatb
   18. odulat
   19. poslubmo
   20. posglbmo
   21. poslubd
   22. poslubdg
   23. posglbd
4. Subset order structures
   1. cipo
   2. df-ipo
   3. ipostr
   4. ipoval
   5. ipobas
   6. ipolerval
   7. ipotset
   8. ipole
   9. ipolt
   10. ipopos
   11. isipodrs
   12. ipodrscl
   13. ipodrsfi
   14. fpwipodrs
   15. ipodrsima
   16. isacs3lem
   17. acsdrsel
   18. isacs4lem
   19. isacs5lem
   20. acsdrscl
   21. acsficl
   22. isacs5
   23. isacs4
   24. isacs3
   25. acsficld
   26. acsficl2d
   27. acsfiindd
   28. acsmapd
   29. acsmap2d
   30. acsinfd
   31. acsdomd
   32. acsinfdimd
   33. acsexdimd
   34. mrelatglb
   35. mrelatglb0
   36. mrelatlub
   37. mreclatBAD
5. Distributive lattices
   1. latmass
   2. latdisdlem
   3. latdisd
   4. cdlat
   5. df-dlat
   6. isdlat
   7. dlatmjdi
   8. dlatl
   9. odudlatb
   10. dlatjmdi
6. Posets and lattices as relations
   1. cps
   2. ctsr
   3. df-ps
   4. df-tsr
   5. isps
   6. psrel
   7. psref2
   8. pstr2
   9. pslem
   10. psdmrn
   11. psref
   12. psrn
   13. psasym
   14. pstr
   15. cnvps
   16. cnvpsb
   17. psss
   18. psssdm2
   19. psssdm
   20. istsr
   21. istsr2
   22. tsrlin
   23. tsrlemax
   24. tsrps
   25. cnvtsr
   26. tsrss
   27. ledm
   28. lern
   29. lefld
   30. letsr
7. Directed sets, nets
   1. cdir
   2. ctail
   3. df-dir
   4. df-tail
   5. isdir
   6. reldir
   7. dirdm
   8. dirref
   9. dirtr
   10. dirge
   11. tsrdir