Metamath Proof Explorer
Table of Contents - 20.44.13.2. Preordered sets as thin categories
- cprstc
- df-prstc
- prstcval
- prstcnidlem
- prstcnid
- prstcbas
- prstcleval
- prstclevalOLD
- prstcle
- prstcocval
- prstcocvalOLD
- prstcoc
- prstchomval
- prstcprs
- prstcthin
- prstchom
- prstchom2
- prstchom2ALT
- postcpos
- postcposALT
- postc