Metamath Proof Explorer
Table of Contents - 9.6. Posets, directed sets, and lattices as relations
- Posets and lattices as relations
- cps
- ctsr
- df-ps
- df-tsr
- isps
- psrel
- psref2
- pstr2
- pslem
- psdmrn
- psref
- psrn
- psasym
- pstr
- cnvps
- cnvpsb
- psss
- psssdm2
- psssdm
- istsr
- istsr2
- tsrlin
- tsrlemax
- tsrps
- cnvtsr
- tsrss
- ledm
- lern
- lefld
- letsr
- Directed sets, nets
- cdir
- ctail
- df-dir
- df-tail
- isdir
- reldir
- dirdm
- dirref
- dirtr
- dirge
- tsrdir