Metamath Proof Explorer


Table of Contents - 12.1.1. Topological spaces

A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union, see toponuni), and it may sometimes be more convenient to consider topologies without reference to the underlying set. This is why we define successively the class of topologies (df-top), then the function which associates with a set the set of topologies on it (df-topon), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp). Of course, a topology is the same thing as a topology on a set (see toprntopon).

  1. Topologies
    1. ctop
    2. df-top
    3. istopg
    4. istop2g
    5. uniopn
    6. iunopn
    7. inopn
    8. fitop
    9. fiinopn
    10. iinopn
    11. unopn
    12. 0opn
    13. 0ntop
    14. topopn
    15. eltopss
    16. riinopn
    17. rintopn
  2. Topologies on sets
    1. ctopon
    2. df-topon
    3. istopon
    4. topontop
    5. toponuni
    6. topontopi
    7. toponunii
    8. toptopon
    9. toptopon2
    10. topontopon
    11. funtopon
    12. toponrestid
    13. toponsspwpw
    14. dmtopon
    15. fntopon
    16. toprntopon
    17. toponmax
    18. toponss
    19. toponcom
    20. toponcomb
    21. topgele
    22. topsn
  3. Topological spaces
    1. ctps
    2. df-topsp
    3. istps
    4. istps2
    5. tpsuni
    6. tpstop
    7. tpspropd
    8. tpsprop2d
    9. topontopn
    10. tsettps
    11. istpsi
    12. eltpsg
    13. eltpsi