Metamath Proof Explorer

Table of Contents - 9.6. Posets, directed sets, and lattices as relations

1. 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
2. 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
3. Chains
   1. cchn
   2. df-chn
   3. ischn
   4. chnwrd
   5. chnltm1
   6. pfxchn
   7. nfchnd
   8. chneq1
   9. chneq2
   10. chneq12
   11. chnrss
   12. chndss
   13. chnrdss
   14. chnexg
   15. nulchn
   16. s1chn
   17. chnind
   18. chnub
   19. chnlt
   20. chnso
   21. chnccats1
   22. chnccat
   23. chnrev
   24. chnflenfi
   25. chnf
   26. chnpof1
   27. chnpoadomd
   28. chnpolleha
   29. chnpolfz
   30. chnfi
   31. chninf
   32. chnfibg
   33. ex-chn1
   34. ex-chn2