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