Metamath Proof Explorer

Table of Contents - 12.1. Topology

1. Topological spaces
   1. Topologies
   2. Topologies on sets
   3. Topological spaces
2. Topological bases
   1. ctb
   2. df-bases
   3. isbasisg
   4. isbasis2g
   5. isbasis3g
   6. basis1
   7. basis2
   8. fiinbas
   9. basdif0
   10. baspartn
   11. tgval
   12. tgval2
   13. eltg
   14. eltg2
   15. eltg2b
   16. eltg4i
   17. eltg3i
   18. eltg3
   19. tgval3
   20. tg1
   21. tg2
   22. bastg
   23. unitg
   24. tgss
   25. tgcl
   26. tgclb
   27. tgtopon
   28. topbas
   29. tgtop
   30. eltop
   31. eltop2
   32. eltop3
   33. fibas
   34. tgdom
   35. tgiun
   36. tgidm
   37. bastop
   38. tgtop11
   39. 0top
   40. en1top
   41. en2top
   42. tgss3
   43. tgss2
   44. basgen
   45. basgen2
   46. 2basgen
   47. tgfiss
   48. tgdif0
   49. bastop1
   50. bastop2
3. Examples of topologies
   1. distop
   2. topnex
   3. distopon
   4. sn0topon
   5. sn0top
   6. indislem
   7. indistopon
   8. indistop
   9. indisuni
   10. fctop
   11. fctop2
   12. cctop
   13. ppttop
   14. pptbas
   15. epttop
   16. indistpsx
   17. indistps
   18. indistps2
   19. indistpsALT
   20. indistps2ALT
   21. distps
4. Closure and interior
   1. ccld
   2. cnt
   3. ccl
   4. df-cld
   5. df-ntr
   6. df-cls
   7. fncld
   8. cldval
   9. ntrfval
   10. clsfval
   11. cldrcl
   12. iscld
   13. iscld2
   14. cldss
   15. cldss2
   16. cldopn
   17. isopn2
   18. opncld
   19. difopn
   20. topcld
   21. ntrval
   22. clsval
   23. 0cld
   24. iincld
   25. intcld
   26. uncld
   27. cldcls
   28. incld
   29. riincld
   30. iuncld
   31. unicld
   32. clscld
   33. clsf
   34. ntropn
   35. clsval2
   36. ntrval2
   37. ntrdif
   38. clsdif
   39. clsss
   40. ntrss
   41. sscls
   42. ntrss2
   43. ssntr
   44. clsss3
   45. ntrss3
   46. ntrin
   47. cmclsopn
   48. cmntrcld
   49. iscld3
   50. iscld4
   51. isopn3
   52. clsidm
   53. ntridm
   54. clstop
   55. ntrtop
   56. 0ntr
   57. clsss2
   58. elcls
   59. elcls2
   60. clsndisj
   61. ntrcls0
   62. ntreq0
   63. cldmre
   64. mrccls
   65. cls0
   66. ntr0
   67. isopn3i
   68. elcls3
   69. opncldf1
   70. opncldf2
   71. opncldf3
   72. isclo
   73. isclo2
   74. discld
   75. sn0cld
   76. indiscld
   77. mretopd
   78. toponmre
   79. cldmreon
   80. iscldtop
   81. mreclatdemoBAD
5. Neighborhoods
   1. cnei
   2. df-nei
   3. neifval
   4. neif
   5. neiss2
   6. neival
   7. isnei
   8. neiint
   9. isneip
   10. neii1
   11. neisspw
   12. neii2
   13. neiss
   14. ssnei
   15. elnei
   16. 0nnei
   17. neips
   18. opnneissb
   19. opnssneib
   20. ssnei2
   21. neindisj
   22. opnneiss
   23. opnneip
   24. opnnei
   25. tpnei
   26. neiuni
   27. neindisj2
   28. topssnei
   29. innei
   30. opnneiid
   31. neissex
   32. 0nei
   33. neipeltop
   34. neiptopuni
   35. neiptoptop
   36. neiptopnei
   37. neiptopreu
6. Limit points and perfect sets
   1. clp
   2. cperf
   3. df-lp
   4. df-perf
   5. lpfval
   6. lpval
   7. islp
   8. lpsscls
   9. lpss
   10. lpdifsn
   11. lpss3
   12. islp2
   13. islp3
   14. maxlp
   15. clslp
   16. islpi
   17. cldlp
   18. isperf
   19. isperf2
   20. isperf3
   21. perflp
   22. perfi
   23. perftop
7. Subspace topologies
   1. restrcl
   2. restbas
   3. tgrest
   4. resttop
   5. resttopon
   6. restuni
   7. stoig
   8. restco
   9. restabs
   10. restin
   11. restuni2
   12. resttopon2
   13. rest0
   14. restsn
   15. restsn2
   16. restcld
   17. restcldi
   18. restcldr
   19. restopnb
   20. ssrest
   21. restopn2
   22. restdis
   23. restfpw
   24. neitr
   25. restcls
   26. restntr
   27. restlp
   28. restperf
   29. perfopn
   30. resstopn
   31. resstps
8. Order topology
   1. ordtbaslem
   2. ordtval
   3. ordtuni
   4. ordtbas2
   5. ordtbas
   6. ordttopon
   7. ordtopn1
   8. ordtopn2
   9. ordtopn3
   10. ordtcld1
   11. ordtcld2
   12. ordtcld3
   13. ordttop
   14. ordtcnv
   15. ordtrest
   16. ordtrest2lem
   17. ordtrest2
   18. letopon
   19. letop
   20. letopuni
   21. xrstopn
   22. xrstps
   23. leordtvallem1
   24. leordtvallem2
   25. leordtval2
   26. leordtval
   27. iccordt
   28. iocpnfordt
   29. icomnfordt
   30. iooordt
   31. reordt
   32. lecldbas
   33. pnfnei
   34. mnfnei
   35. ordtrestixx
   36. ordtresticc
9. Limits and continuity in topological spaces
   1. ccn
   2. ccnp
   3. clm
   4. df-cn
   5. df-cnp
   6. df-lm
   7. lmrel
   8. lmrcl
   9. lmfval
   10. cnfval
   11. cnpfval
   12. iscn
   13. cnpval
   14. iscnp
   15. iscn2
   16. iscnp2
   17. cntop1
   18. cntop2
   19. cnptop1
   20. cnptop2
   21. iscnp3
   22. cnprcl
   23. cnf
   24. cnpf
   25. cnpcl
   26. cnf2
   27. cnpf2
   28. cnprcl2
   29. tgcn
   30. tgcnp
   31. subbascn
   32. ssidcn
   33. cnpimaex
   34. idcn
   35. lmbr
   36. lmbr2
   37. lmbrf
   38. lmconst
   39. lmcvg
   40. iscnp4
   41. cnpnei
   42. cnima
   43. cnco
   44. cnpco
   45. cnclima
   46. iscncl
   47. cncls2i
   48. cnntri
   49. cnclsi
   50. cncls2
   51. cncls
   52. cnntr
   53. cnss1
   54. cnss2
   55. cncnpi
   56. cnsscnp
   57. cncnp
   58. cncnp2
   59. cnnei
   60. cnconst2
   61. cnconst
   62. cnrest
   63. cnrest2
   64. cnrest2r
   65. cnpresti
   66. cnprest
   67. cnprest2
   68. cndis
   69. cnindis
   70. cnpdis
   71. paste
   72. lmfpm
   73. lmfss
   74. lmcl
   75. lmss
   76. sslm
   77. lmres
   78. lmff
   79. lmcls
   80. lmcld
   81. lmcnp
   82. lmcn
10. Separated spaces: T0, T1, T2 (Hausdorff) ...
    1. ct0
    2. ct1
    3. cha
    4. creg
    5. cnrm
    6. ccnrm
    7. cpnrm
    8. df-t0
    9. df-t1
    10. df-haus
    11. df-reg
    12. df-nrm
    13. df-cnrm
    14. df-pnrm
    15. ist0
    16. ist1
    17. ishaus
    18. iscnrm
    19. t0sep
    20. t0dist
    21. t1sncld
    22. t1ficld
    23. hausnei
    24. t0top
    25. t1top
    26. haustop
    27. isreg
    28. regtop
    29. regsep
    30. isnrm
    31. nrmtop
    32. cnrmtop
    33. iscnrm2
    34. ispnrm
    35. pnrmnrm
    36. pnrmtop
    37. pnrmcld
    38. pnrmopn
    39. ist0-2
    40. ist0-3
    41. cnt0
    42. ist1-2
    43. t1t0
    44. ist1-3
    45. cnt1
    46. ishaus2
    47. haust1
    48. hausnei2
    49. cnhaus
    50. nrmsep3
    51. nrmsep2
    52. nrmsep
    53. isnrm2
    54. isnrm3
    55. cnrmi
    56. cnrmnrm
    57. restcnrm
    58. resthauslem
    59. lpcls
    60. perfcls
    61. restt0
    62. restt1
    63. resthaus
    64. t1sep2
    65. t1sep
    66. sncld
    67. sshauslem
    68. sst0
    69. sst1
    70. sshaus
    71. regsep2
    72. isreg2
    73. dnsconst
    74. ordtt1
    75. lmmo
    76. lmfun
    77. dishaus
    78. ordthauslem
    79. ordthaus
    80. xrhaus
11. Compactness
    1. ccmp
    2. df-cmp
    3. iscmp
    4. cmpcov
    5. cmpcov2
    6. cmpcovf
    7. cncmp
    8. fincmp
    9. 0cmp
    10. cmptop
    11. rncmp
    12. imacmp
    13. discmp
    14. cmpsublem
    15. cmpsub
    16. tgcmp
    17. cmpcld
    18. uncmp
    19. fiuncmp
    20. sscmp
    21. hauscmplem
    22. hauscmp
    23. cmpfi
    24. cmpfii
12. Bolzano-Weierstrass theorem
    1. bwth
13. Connectedness
    1. cconn
    2. df-conn
    3. isconn
    4. isconn2
    5. connclo
    6. conndisj
    7. conntop
    8. indisconn
    9. dfconn2
    10. connsuba
    11. connsub
    12. cnconn
    13. nconnsubb
    14. connsubclo
    15. connima
    16. conncn
    17. iunconnlem
    18. iunconn
    19. unconn
    20. clsconn
    21. conncompid
    22. conncompconn
    23. conncompss
    24. conncompcld
    25. conncompclo
    26. t1connperf
14. First- and second-countability
    1. c1stc
    2. c2ndc
    3. df-1stc
    4. df-2ndc
    5. is1stc
    6. is1stc2
    7. 1stctop
    8. 1stcclb
    9. 1stcfb
    10. is2ndc
    11. 2ndctop
    12. 2ndci
    13. 2ndcsb
    14. 2ndcredom
    15. 2ndc1stc
    16. 1stcrestlem
    17. 1stcrest
    18. 2ndcrest
    19. 2ndcctbss
    20. 2ndcdisj
    21. 2ndcdisj2
    22. 2ndcomap
    23. 2ndcsep
    24. dis2ndc
    25. 1stcelcls
    26. 1stccnp
    27. 1stccn
15. Local topological properties
    1. clly
    2. cnlly
    3. df-lly
    4. df-nlly
    5. islly
    6. isnlly
    7. llyeq
    8. nllyeq
    9. llytop
    10. nllytop
    11. llyi
    12. nllyi
    13. nlly2i
    14. llynlly
    15. llyssnlly
    16. llyss
    17. nllyss
    18. subislly
    19. restnlly
    20. restlly
    21. islly2
    22. llyrest
    23. nllyrest
    24. loclly
    25. llyidm
    26. nllyidm
    27. toplly
    28. topnlly
    29. hauslly
    30. hausnlly
    31. hausllycmp
    32. cldllycmp
    33. lly1stc
    34. dislly
    35. disllycmp
    36. dis1stc
    37. hausmapdom
    38. hauspwdom
16. Refinements
    1. cref
    2. cptfin
    3. clocfin
    4. df-ref
    5. df-ptfin
    6. df-locfin
    7. refrel
    8. isref
    9. refbas
    10. refssex
    11. ssref
    12. refref
    13. reftr
    14. refun0
    15. isptfin
    16. islocfin
    17. finptfin
    18. ptfinfin
    19. finlocfin
    20. locfintop
    21. locfinbas
    22. locfinnei
    23. lfinpfin
    24. lfinun
    25. locfincmp
    26. unisngl
    27. dissnref
    28. dissnlocfin
    29. locfindis
    30. locfincf
    31. comppfsc
17. Compactly generated spaces
    1. ckgen
    2. df-kgen
    3. kgenval
    4. elkgen
    5. kgeni
    6. kgentopon
    7. kgenuni
    8. kgenftop
    9. kgenf
    10. kgentop
    11. kgenss
    12. kgenhaus
    13. kgencmp
    14. kgencmp2
    15. kgenidm
    16. iskgen2
    17. iskgen3
    18. llycmpkgen2
    19. cmpkgen
    20. llycmpkgen
    21. 1stckgenlem
    22. 1stckgen
    23. kgen2ss
    24. kgencn
    25. kgencn2
    26. kgencn3
    27. kgen2cn
18. Product topologies
    1. ctx
    2. cxko
    3. df-tx
    4. df-xko
    5. txval
    6. txuni2
    7. txbasex
    8. txbas
    9. eltx
    10. txtop
    11. ptval
    12. ptpjpre1
    13. elpt
    14. elptr
    15. elptr2
    16. ptbasid
    17. ptuni2
    18. ptbasin
    19. ptbasin2
    20. ptbas
    21. ptpjpre2
    22. ptbasfi
    23. pttop
    24. ptopn
    25. ptopn2
    26. xkotf
    27. xkobval
    28. xkoval
    29. xkotop
    30. xkoopn
    31. txtopi
    32. txtopon
    33. txuni
    34. txunii
    35. ptuni
    36. ptunimpt
    37. pttopon
    38. pttoponconst
    39. ptuniconst
    40. xkouni
    41. xkotopon
    42. ptval2
    43. txopn
    44. txcld
    45. txcls
    46. txss12
    47. txbasval
    48. neitx
    49. txcnpi
    50. tx1cn
    51. tx2cn
    52. ptpjcn
    53. ptpjopn
    54. ptcld
    55. ptcldmpt
    56. ptclsg
    57. ptcls
    58. dfac14lem
    59. dfac14
    60. xkoccn
    61. txcnp
    62. ptcnplem
    63. ptcnp
    64. upxp
    65. txcnmpt
    66. uptx
    67. txcn
    68. ptcn
    69. prdstopn
    70. prdstps
    71. pwstps
    72. txrest
    73. txdis
    74. txindislem
    75. txindis
    76. txdis1cn
    77. txlly
    78. txnlly
    79. pthaus
    80. ptrescn
    81. txtube
    82. txcmplem1
    83. txcmplem2
    84. txcmp
    85. txcmpb
    86. hausdiag
    87. hauseqlcld
    88. txhaus
    89. txlm
    90. lmcn2
    91. tx1stc
    92. tx2ndc
    93. txkgen
    94. xkohaus
    95. xkoptsub
    96. xkopt
    97. xkopjcn
    98. xkoco1cn
    99. xkoco2cn
    100. xkococnlem
    101. xkococn
19. Continuous function-builders
    1. cnmptid
    2. cnmptc
    3. cnmpt11
    4. cnmpt11f
    5. cnmpt1t
    6. cnmpt12f
    7. cnmpt12
    8. cnmpt1st
    9. cnmpt2nd
    10. cnmpt2c
    11. cnmpt21
    12. cnmpt21f
    13. cnmpt2t
    14. cnmpt22
    15. cnmpt22f
    16. cnmpt1res
    17. cnmpt2res
    18. cnmptcom
    19. cnmptkc
    20. cnmptkp
    21. cnmptk1
    22. cnmpt1k
    23. cnmptkk
    24. xkofvcn
    25. cnmptk1p
    26. cnmptk2
    27. xkoinjcn
    28. cnmpt2k
    29. txconn
    30. imasnopn
    31. imasncld
    32. imasncls
20. Quotient maps and quotient topology
    1. ckq
    2. df-kq
    3. qtopval
    4. qtopval2
    5. elqtop
    6. qtopres
    7. qtoptop2
    8. qtoptop
    9. elqtop2
    10. qtopuni
    11. elqtop3
    12. qtoptopon
    13. qtopid
    14. idqtop
    15. qtopcmplem
    16. qtopcmp
    17. qtopconn
    18. qtopkgen
    19. basqtop
    20. tgqtop
    21. qtopcld
    22. qtopcn
    23. qtopss
    24. qtopeu
    25. qtoprest
    26. qtopomap
    27. qtopcmap
    28. imastopn
    29. imastps
    30. qustps
    31. kqfval
    32. kqfeq
    33. kqffn
    34. kqval
    35. kqtopon
    36. kqid
    37. ist0-4
    38. kqfvima
    39. kqsat
    40. kqdisj
    41. kqcldsat
    42. kqopn
    43. kqcld
    44. kqt0lem
    45. isr0
    46. r0cld
    47. regr1lem
    48. regr1lem2
    49. kqreglem1
    50. kqreglem2
    51. kqnrmlem1
    52. kqnrmlem2
    53. kqtop
    54. kqt0
    55. kqf
    56. r0sep
    57. nrmr0reg
    58. regr1
    59. kqreg
    60. kqnrm
21. Homeomorphisms
    1. chmeo
    2. chmph
    3. df-hmeo
    4. df-hmph
    5. hmeofn
    6. hmeofval
    7. ishmeo
    8. hmeocn
    9. hmeocnvcn
    10. hmeocnv
    11. hmeof1o2
    12. hmeof1o
    13. hmeoima
    14. hmeoopn
    15. hmeocld
    16. hmeocls
    17. hmeontr
    18. hmeoimaf1o
    19. hmeores
    20. hmeoco
    21. idhmeo
    22. hmeocnvb
    23. hmeoqtop
    24. hmph
    25. hmphi
    26. hmphtop
    27. hmphtop1
    28. hmphtop2
    29. hmphref
    30. hmphsym
    31. hmphtr
    32. hmpher
    33. hmphen
    34. hmphsymb
    35. haushmphlem
    36. cmphmph
    37. connhmph
    38. t0hmph
    39. t1hmph
    40. haushmph
    41. reghmph
    42. nrmhmph
    43. hmph0
    44. hmphdis
    45. hmphindis
    46. indishmph
    47. hmphen2
    48. cmphaushmeo
    49. ordthmeolem
    50. ordthmeo
    51. txhmeo
    52. txswaphmeolem
    53. txswaphmeo
    54. pt1hmeo
    55. ptuncnv
    56. ptunhmeo
    57. xpstopnlem1
    58. xpstps
    59. xpstopnlem2
    60. xpstopn
    61. ptcmpfi
    62. xkocnv
    63. xkohmeo
    64. qtopf1
    65. qtophmeo
    66. t0kq
    67. kqhmph
    68. ist1-5lem
    69. t1r0
    70. ist1-5
    71. ishaus3
    72. nrmreg
    73. reghaus
    74. nrmhaus