Metamath Proof Explorer
Table of Contents - 9.6.1. Posets and lattices as relations
See commented-out notes for 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