Metamath Proof Explorer

Table of Contents - 9.4. Totally ordered sets (tosets)

1. ctos
2. df-toset
3. istos
4. tosso
5. tospos
6. tleile
7. tltnle
8. cp0
9. cp1
10. df-p0
11. df-p1
12. p0val
13. p1val
14. p0le
15. ple1