Metamath Proof Explorer

Table of Contents - 20.33.4. Exploring Topology via Seifert and Threlfall

See Seifert and Threlfall: A Textbook Of Topology (1980) which is an English translation of Lehrbuch der Topologie (1934).

1. Equinumerosity of sets of relations and maps
   1. enrelmap
   2. enrelmapr
   3. enmappw
   4. enmappwid
   5. rfovd
   6. rfovfvd
   7. rfovfvfvd
   8. rfovcnvf1od
   9. rfovcnvd
   10. rfovf1od
   11. rfovcnvfvd
   12. fsovd
   13. fsovrfovd
   14. fsovfvd
   15. fsovfvfvd
   16. fsovfd
   17. fsovcnvlem
   18. fsovcnvd
   19. fsovcnvfvd
   20. fsovf1od
   21. dssmapfvd
   22. dssmapfv2d
   23. dssmapfv3d
   24. dssmapnvod
   25. dssmapf1od
   26. dssmap2d
2. Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
   1. or3or
   2. andi3or
   3. uneqsn
   4. df3o2
   5. df3o3
   6. brfvimex
   7. brovmptimex
   8. brovmptimex1
   9. brovmptimex2
   10. brcoffn
   11. brcofffn
   12. brco2f1o
   13. brco3f1o
   14. ntrclsbex
   15. ntrclsrcomplex
   16. neik0imk0p
   17. ntrk2imkb
   18. ntrkbimka
   19. ntrk0kbimka
   20. clsk3nimkb
   21. clsk1indlem0
   22. clsk1indlem2
   23. clsk1indlem3
   24. clsk1indlem4
   25. clsk1indlem1
   26. clsk1independent
   27. neik0pk1imk0
   28. isotone1
   29. isotone2
   30. ntrk1k3eqk13
   31. ntrclsf1o
   32. ntrclsnvobr
   33. ntrclsiex
   34. ntrclskex
   35. ntrclsfv1
   36. ntrclsfv2
   37. ntrclselnel1
   38. ntrclselnel2
   39. ntrclsfv
   40. ntrclsfveq1
   41. ntrclsfveq2
   42. ntrclsfveq
   43. ntrclsss
   44. ntrclsneine0lem
   45. ntrclsneine0
   46. ntrclscls00
   47. ntrclsiso
   48. ntrclsk2
   49. ntrclskb
   50. ntrclsk3
   51. ntrclsk13
   52. ntrclsk4
   53. ntrneibex
   54. ntrneircomplex
   55. ntrneif1o
   56. ntrneiiex
   57. ntrneinex
   58. ntrneicnv
   59. ntrneifv1
   60. ntrneifv2
   61. ntrneiel
   62. ntrneifv3
   63. ntrneineine0lem
   64. ntrneineine1lem
   65. ntrneifv4
   66. ntrneiel2
   67. ntrneineine0
   68. ntrneineine1
   69. ntrneicls00
   70. ntrneicls11
   71. ntrneiiso
   72. ntrneik2
   73. ntrneix2
   74. ntrneikb
   75. ntrneixb
   76. ntrneik3
   77. ntrneix3
   78. ntrneik13
   79. ntrneix13
   80. ntrneik4w
   81. ntrneik4
   82. clsneibex
   83. clsneircomplex
   84. clsneif1o
   85. clsneicnv
   86. clsneikex
   87. clsneinex
   88. clsneiel1
   89. clsneiel2
   90. clsneifv3
   91. clsneifv4
   92. neicvgbex
   93. neicvgrcomplex
   94. neicvgf1o
   95. neicvgnvo
   96. neicvgnvor
   97. neicvgmex
   98. neicvgnex
   99. neicvgel1
   100. neicvgel2
   101. neicvgfv
   102. ntrrn
   103. ntrf
   104. ntrf2
   105. ntrelmap
   106. clsf2
   107. clselmap
   108. dssmapntrcls
   109. dssmapclsntr
3. Generic Neighborhood Spaces
   1. gneispa
   2. gneispb
   3. gneispace2
   4. gneispace3
   5. gneispace
   6. gneispacef
   7. gneispacef2
   8. gneispacefun
   9. gneispacern
   10. gneispacern2
   11. gneispace0nelrn
   12. gneispace0nelrn2
   13. gneispace0nelrn3
   14. gneispaceel
   15. gneispaceel2
   16. gneispacess
   17. gneispacess2