Metamath Proof Explorer

Table of Contents - 20.13. Mathbox for Chen-Pang He

1. Ordinal topology
   1. ontopbas
   2. onsstopbas
   3. onpsstopbas
   4. ontgval
   5. ontgsucval
   6. onsuctop
   7. onsuctopon
   8. ordtoplem
   9. ordtop
   10. onsucconni
   11. onsucconn
   12. ordtopconn
   13. onintopssconn
   14. onsuct0
   15. ordtopt0
   16. onsucsuccmpi
   17. onsucsuccmp
   18. limsucncmpi
   19. limsucncmp
   20. ordcmp
   21. ssoninhaus
   22. onint1
   23. oninhaus