Metamath Proof Explorer

Table of Contents - 9.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