Metamath Proof Explorer

Table of Contents - 12.4. Metric spaces

1. Pseudometric spaces
   1. ispsmet
   2. psmetdmdm
   3. psmetf
   4. psmetcl
   5. psmet0
   6. psmettri2
   7. psmetsym
   8. psmettri
   9. psmetge0
   10. psmetxrge0
   11. psmetres2
   12. psmetlecl
   13. distspace
2. Basic metric space properties
   1. cxms
   2. cms
   3. ctms
   4. df-xms
   5. df-ms
   6. df-tms
   7. ismet
   8. isxmet
   9. ismeti
   10. isxmetd
   11. isxmet2d
   12. metflem
   13. xmetf
   14. metf
   15. xmetcl
   16. metcl
   17. ismet2
   18. metxmet
   19. xmetdmdm
   20. metdmdm
   21. xmetunirn
   22. xmeteq0
   23. meteq0
   24. xmettri2
   25. mettri2
   26. xmet0
   27. met0
   28. xmetge0
   29. metge0
   30. xmetlecl
   31. xmetsym
   32. xmetpsmet
   33. xmettpos
   34. metsym
   35. xmettri
   36. mettri
   37. xmettri3
   38. mettri3
   39. xmetrtri
   40. xmetrtri2
   41. metrtri
   42. xmetgt0
   43. metgt0
   44. metn0
   45. xmetres2
   46. metreslem
   47. metres2
   48. xmetres
   49. metres
   50. 0met
   51. prdsdsf
   52. prdsxmetlem
   53. prdsxmet
   54. prdsmet
   55. ressprdsds
   56. resspwsds
   57. imasdsf1olem
   58. imasdsf1o
   59. imasf1oxmet
   60. imasf1omet
   61. xpsdsfn
   62. xpsdsfn2
   63. xpsxmetlem
   64. xpsxmet
   65. xpsdsval
   66. xpsmet
3. Metric space balls
   1. blfvalps
   2. blfval
   3. blvalps
   4. blval
   5. elblps
   6. elbl
   7. elbl2ps
   8. elbl2
   9. elbl3ps
   10. elbl3
   11. blcomps
   12. blcom
   13. xblpnfps
   14. xblpnf
   15. blpnf
   16. bldisj
   17. blgt0
   18. bl2in
   19. xblss2ps
   20. xblss2
   21. blss2ps
   22. blss2
   23. blhalf
   24. blfps
   25. blf
   26. blrnps
   27. blrn
   28. xblcntrps
   29. xblcntr
   30. blcntrps
   31. blcntr
   32. xbln0
   33. bln0
   34. blelrnps
   35. blelrn
   36. blssm
   37. unirnblps
   38. unirnbl
   39. blin
   40. ssblps
   41. ssbl
   42. blssps
   43. blss
   44. blssexps
   45. blssex
   46. ssblex
   47. blin2
   48. blbas
   49. blres
   50. xmeterval
   51. xmeter
   52. xmetec
   53. blssec
   54. blpnfctr
   55. xmetresbl
4. Open sets of a metric space
   1. mopnval
   2. mopntopon
   3. mopntop
   4. mopnuni
   5. elmopn
   6. mopnfss
   7. mopnm
   8. elmopn2
   9. mopnss
   10. isxms
   11. isxms2
   12. isms
   13. isms2
   14. xmstopn
   15. mstopn
   16. xmstps
   17. msxms
   18. mstps
   19. xmsxmet
   20. msmet
   21. msf
   22. xmsxmet2
   23. msmet2
   24. mscl
   25. xmscl
   26. xmsge0
   27. xmseq0
   28. xmssym
   29. xmstri2
   30. mstri2
   31. xmstri
   32. mstri
   33. xmstri3
   34. mstri3
   35. msrtri
   36. xmspropd
   37. mspropd
   38. setsmsbas
   39. setsmsbasOLD
   40. setsmsds
   41. setsmsdsOLD
   42. setsmstset
   43. setsmstopn
   44. setsxms
   45. setsms
   46. tmsval
   47. tmslem
   48. tmslemOLD
   49. tmsbas
   50. tmsds
   51. tmstopn
   52. tmsxms
   53. tmsms
   54. imasf1obl
   55. imasf1oxms
   56. imasf1oms
   57. prdsbl
   58. mopni
   59. mopni2
   60. mopni3
   61. blssopn
   62. unimopn
   63. mopnin
   64. mopn0
   65. rnblopn
   66. blopn
   67. neibl
   68. blnei
   69. lpbl
   70. blsscls2
   71. blcld
   72. blcls
   73. blsscls
   74. metss
   75. metequiv
   76. metequiv2
   77. metss2lem
   78. metss2
   79. comet
   80. stdbdmetval
   81. stdbdxmet
   82. stdbdmet
   83. stdbdbl
   84. stdbdmopn
   85. mopnex
   86. methaus
   87. met1stc
   88. met2ndci
   89. met2ndc
   90. metrest
   91. ressxms
   92. ressms
   93. prdsmslem1
   94. prdsxmslem1
   95. prdsxmslem2
   96. prdsxms
   97. prdsms
   98. pwsxms
   99. pwsms
   100. xpsxms
   101. xpsms
   102. tmsxps
   103. tmsxpsmopn
   104. tmsxpsval
   105. tmsxpsval2
5. Continuity in metric spaces
   1. metcnp3
   2. metcnp
   3. metcnp2
   4. metcn
   5. metcnpi
   6. metcnpi2
   7. metcnpi3
   8. txmetcnp
   9. txmetcn
6. The uniform structure generated by a metric
   1. metuval
   2. metustel
   3. metustss
   4. metustrel
   5. metustto
   6. metustid
   7. metustsym
   8. metustexhalf
   9. metustfbas
   10. metust
   11. cfilucfil
   12. metuust
   13. cfilucfil2
   14. blval2
   15. elbl4
   16. metuel
   17. metuel2
   18. metustbl
   19. psmetutop
   20. xmetutop
   21. xmsusp
   22. restmetu
   23. metucn
7. Examples of metric spaces
   1. dscmet
   2. dscopn
   3. nrmmetd
   4. abvmet
8. Normed algebraic structures
   1. cnm
   2. cngp
   3. ctng
   4. cnrg
   5. cnlm
   6. cnvc
   7. df-nm
   8. df-ngp
   9. df-tng
   10. df-nrg
   11. df-nlm
   12. df-nvc
   13. nmfval
   14. nmval
   15. nmfval0
   16. nmfval2
   17. nmval2
   18. nmf2
   19. nmpropd
   20. nmpropd2
   21. isngp
   22. isngp2
   23. isngp3
   24. ngpgrp
   25. ngpms
   26. ngpxms
   27. ngptps
   28. ngpmet
   29. ngpds
   30. ngpdsr
   31. ngpds2
   32. ngpds2r
   33. ngpds3
   34. ngpds3r
   35. ngprcan
   36. ngplcan
   37. isngp4
   38. ngpinvds
   39. ngpsubcan
   40. nmf
   41. nmcl
   42. nmge0
   43. nmeq0
   44. nmne0
   45. nmrpcl
   46. nminv
   47. nmmtri
   48. nmsub
   49. nmrtri
   50. nm2dif
   51. nmtri
   52. nmtri2
   53. ngpi
   54. nm0
   55. nmgt0
   56. sgrim
   57. sgrimval
   58. subgnm
   59. subgnm2
   60. subgngp
   61. ngptgp
   62. ngppropd
   63. reldmtng
   64. tngval
   65. tnglem
   66. tnglemOLD
   67. tngbas
   68. tngbasOLD
   69. tngplusg
   70. tngplusgOLD
   71. tng0
   72. tngmulr
   73. tngmulrOLD
   74. tngsca
   75. tngscaOLD
   76. tngvsca
   77. tngvscaOLD
   78. tngip
   79. tngipOLD
   80. tngds
   81. tngdsOLD
   82. tngtset
   83. tngtopn
   84. tngnm
   85. tngngp2
   86. tngngpd
   87. tngngp
   88. tnggrpr
   89. tngngp3
   90. nrmtngdist
   91. nrmtngnrm
   92. tngngpim
   93. isnrg
   94. nrgabv
   95. nrgngp
   96. nrgring
   97. nmmul
   98. nrgdsdi
   99. nrgdsdir
   100. nm1
   101. unitnmn0
   102. nminvr
   103. nmdvr
   104. nrgdomn
   105. nrgtgp
   106. subrgnrg
   107. tngnrg
   108. isnlm
   109. nmvs
   110. nlmngp
   111. nlmlmod
   112. nlmnrg
   113. nlmngp2
   114. nlmdsdi
   115. nlmdsdir
   116. nlmmul0or
   117. sranlm
   118. nlmvscnlem2
   119. nlmvscnlem1
   120. nlmvscn
   121. rlmnlm
   122. rlmnm
   123. nrgtrg
   124. nrginvrcnlem
   125. nrginvrcn
   126. nrgtdrg
   127. nlmtlm
   128. isnvc
   129. nvcnlm
   130. nvclvec
   131. nvclmod
   132. isnvc2
   133. nvctvc
   134. lssnlm
   135. lssnvc
   136. rlmnvc
   137. ngpocelbl
9. Normed space homomorphisms (bounded linear operators)
   1. cnmo
   2. cnghm
   3. cnmhm
   4. df-nmo
   5. df-nghm
   6. df-nmhm
   7. nmoffn
   8. reldmnghm
   9. reldmnmhm
   10. nmofval
   11. nmoval
   12. nmogelb
   13. nmolb
   14. nmolb2d
   15. nmof
   16. nmocl
   17. nmoge0
   18. nghmfval
   19. isnghm
   20. isnghm2
   21. isnghm3
   22. bddnghm
   23. nghmcl
   24. nmoi
   25. nmoix
   26. nmoi2
   27. nmoleub
   28. nghmrcl1
   29. nghmrcl2
   30. nghmghm
   31. nmo0
   32. nmoeq0
   33. nmoco
   34. nghmco
   35. nmotri
   36. nghmplusg
   37. 0nghm
   38. nmoid
   39. idnghm
   40. nmods
   41. nghmcn
   42. isnmhm
   43. nmhmrcl1
   44. nmhmrcl2
   45. nmhmlmhm
   46. nmhmnghm
   47. nmhmghm
   48. isnmhm2
   49. nmhmcl
   50. idnmhm
   51. 0nmhm
   52. nmhmco
   53. nmhmplusg
10. Topology on the reals
    1. qtopbaslem
    2. qtopbas
    3. retopbas
    4. retop
    5. uniretop
    6. retopon
    7. retps
    8. iooretop
    9. icccld
    10. icopnfcld
    11. iocmnfcld
    12. qdensere
    13. cnmetdval
    14. cnmet
    15. cnxmet
    16. cnbl0
    17. cnblcld
    18. cnfldms
    19. cnfldxms
    20. cnfldtps
    21. cnfldnm
    22. cnngp
    23. cnnrg
    24. cnfldtopn
    25. cnfldtopon
    26. cnfldtop
    27. cnfldhaus
    28. unicntop
    29. cnopn
    30. zringnrg
    31. remetdval
    32. remet
    33. rexmet
    34. bl2ioo
    35. ioo2bl
    36. ioo2blex
    37. blssioo
    38. tgioo
    39. qdensere2
    40. blcvx
    41. rehaus
    42. tgqioo
    43. re2ndc
    44. resubmet
    45. tgioo2
    46. rerest
    47. tgioo3
    48. xrtgioo
    49. xrrest
    50. xrrest2
    51. xrsxmet
    52. xrsdsre
    53. xrsblre
    54. xrsmopn
    55. zcld
    56. recld2
    57. zcld2
    58. zdis
    59. sszcld
    60. reperflem
    61. reperf
    62. cnperf
    63. iccntr
    64. icccmplem1
    65. icccmplem2
    66. icccmplem3
    67. icccmp
    68. reconnlem1
    69. reconnlem2
    70. reconn
    71. retopconn
    72. iccconn
    73. opnreen
    74. rectbntr0
    75. xrge0gsumle
    76. xrge0tsms
    77. xrge0tsms2
    78. metdcnlem
    79. xmetdcn2
    80. xmetdcn
    81. metdcn2
    82. metdcn
    83. msdcn
    84. cnmpt1ds
    85. cnmpt2ds
    86. nmcn
    87. ngnmcncn
    88. abscn
    89. metdsval
    90. metdsf
    91. metdsge
    92. metds0
    93. metdstri
    94. metdsle
    95. metdsre
    96. metdseq0
    97. metdscnlem
    98. metdscn
    99. metdscn2
    100. metnrmlem1a
    101. metnrmlem1
    102. metnrmlem2
    103. metnrmlem3
    104. metnrm
    105. metreg
    106. addcnlem
    107. addcn
    108. subcn
    109. mulcn
    110. divcn
    111. cnfldtgp
    112. fsumcn
    113. fsum2cn
    114. expcn
    115. divccn
    116. sqcn
11. Topological definitions using the reals
    1. cii
    2. ccncf
    3. df-ii
    4. df-cncf
    5. iitopon
    6. iitop
    7. iiuni
    8. dfii2
    9. dfii3
    10. dfii4
    11. dfii5
    12. iicmp
    13. iiconn
    14. cncfval
    15. elcncf
    16. elcncf2
    17. cncfrss
    18. cncfrss2
    19. cncff
    20. cncfi
    21. elcncf1di
    22. elcncf1ii
    23. rescncf
    24. cncffvrn
    25. cncfss
    26. climcncf
    27. abscncf
    28. recncf
    29. imcncf
    30. cjcncf
    31. mulc1cncf
    32. divccncf
    33. cncfco
    34. cncfcompt2
    35. cncfmet
    36. cncfcn
    37. cncfcn1
    38. cncfmptc
    39. cncfmptid
    40. cncfmpt1f
    41. cncfmpt2f
    42. cncfmpt2ss
    43. addccncf
    44. idcncf
    45. sub1cncf
    46. sub2cncf
    47. cdivcncf
    48. negcncf
    49. negfcncf
    50. abscncfALT
    51. cncfcnvcn
    52. expcncf
    53. cnmptre
    54. cnmpopc
    55. iirev
    56. iirevcn
    57. iihalf1
    58. iihalf1cn
    59. iihalf2
    60. iihalf2cn
    61. elii1
    62. elii2
    63. iimulcl
    64. iimulcn
    65. icoopnst
    66. iocopnst
    67. icchmeo
    68. icopnfcnv
    69. icopnfhmeo
    70. iccpnfcnv
    71. iccpnfhmeo
    72. xrhmeo
    73. xrhmph
    74. xrcmp
    75. xrconn
    76. icccvx
    77. oprpiece1res1
    78. oprpiece1res2
    79. cnrehmeo
    80. cnheiborlem
    81. cnheibor
    82. cnllycmp
    83. rellycmp
    84. bndth
    85. evth
    86. evth2
    87. lebnumlem1
    88. lebnumlem2
    89. lebnumlem3
    90. lebnum
    91. xlebnum
    92. lebnumii
12. Path homotopy
    1. chtpy
    2. cphtpy
    3. cphtpc
    4. df-htpy
    5. df-phtpy
    6. ishtpy
    7. htpycn
    8. htpyi
    9. ishtpyd
    10. htpycom
    11. htpyid
    12. htpyco1
    13. htpyco2
    14. htpycc
    15. isphtpy
    16. phtpyhtpy
    17. phtpycn
    18. phtpyi
    19. phtpy01
    20. isphtpyd
    21. isphtpy2d
    22. phtpycom
    23. phtpyid
    24. phtpyco2
    25. phtpycc
    26. df-phtpc
    27. phtpcrel
    28. isphtpc
    29. phtpcer
    30. phtpc01
    31. reparphti
    32. reparpht
    33. phtpcco2
13. The fundamental group
    1. cpco
    2. comi
    3. comn
    4. cpi1
    5. cpin
    6. df-pco
    7. df-om1
    8. df-omn
    9. df-pi1
    10. df-pin
    11. pcofval
    12. pcoval
    13. pcovalg
    14. pcoval1
    15. pco0
    16. pco1
    17. pcoval2
    18. pcocn
    19. copco
    20. pcohtpylem
    21. pcohtpy
    22. pcoptcl
    23. pcopt
    24. pcopt2
    25. pcoass
    26. pcorevcl
    27. pcorevlem
    28. pcorev
    29. pcorev2
    30. pcophtb
    31. om1val
    32. om1bas
    33. om1elbas
    34. om1addcl
    35. om1plusg
    36. om1tset
    37. om1opn
    38. pi1val
    39. pi1bas
    40. pi1blem
    41. pi1buni
    42. pi1bas2
    43. pi1eluni
    44. pi1bas3
    45. pi1cpbl
    46. elpi1
    47. elpi1i
    48. pi1addf
    49. pi1addval
    50. pi1grplem
    51. pi1grp
    52. pi1id
    53. pi1inv
    54. pi1xfrf
    55. pi1xfrval
    56. pi1xfr
    57. pi1xfrcnvlem
    58. pi1xfrcnv
    59. pi1xfrgim
    60. pi1cof
    61. pi1coval
    62. pi1coghm