Metamath Proof Explorer

Table of Contents - 9. BASIC ORDER THEORY

1. Preordered sets and directed sets using extensible structures
   1. cproset
   2. cdrs
   3. df-proset
   4. df-drs
   5. isprs
   6. prslem
   7. prsref
   8. prstr
   9. isdrs
   10. drsdir
   11. drsprs
   12. drsbn0
   13. drsdirfi
   14. isdrs2
2. Posets and lattices using extensible structures
   1. Posets
   2. Lattices
   3. The dual of an ordered set
   4. Subset order structures
   5. Distributive lattices
   6. Posets and lattices as relations
   7. Directed sets, nets