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. setsmsds
   40. setsmstset
   41. setsmstopn
   42. setsxms
   43. setsms
   44. tmsval
   45. tmslem
   46. tmsbas
   47. tmsds
   48. tmstopn
   49. tmsxms
   50. tmsms
   51. imasf1obl
   52. imasf1oxms
   53. imasf1oms
   54. prdsbl
   55. mopni
   56. mopni2
   57. mopni3
   58. blssopn
   59. unimopn
   60. mopnin
   61. mopn0
   62. rnblopn
   63. blopn
   64. neibl
   65. blnei
   66. lpbl
   67. blsscls2
   68. blcld
   69. blcls
   70. blsscls
   71. metss
   72. metequiv
   73. metequiv2
   74. metss2lem
   75. metss2
   76. comet
   77. stdbdmetval
   78. stdbdxmet
   79. stdbdmet
   80. stdbdbl
   81. stdbdmopn
   82. mopnex
   83. methaus
   84. met1stc
   85. met2ndci
   86. met2ndc
   87. metrest
   88. ressxms
   89. ressms
   90. prdsmslem1
   91. prdsxmslem1
   92. prdsxmslem2
   93. prdsxms
   94. prdsms
   95. pwsxms
   96. pwsms
   97. xpsxms
   98. xpsms
   99. tmsxps
   100. tmsxpsmopn
   101. tmsxpsval
   102. 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. tngbas
   67. tngplusg
   68. tng0
   69. tngmulr
   70. tngsca
   71. tngvsca
   72. tngip
   73. tngds
   74. tngtset
   75. tngtopn
   76. tngnm
   77. tngngp2
   78. tngngpd
   79. tngngp
   80. tnggrpr
   81. tngngp3
   82. nrmtngdist
   83. nrmtngnrm
   84. tngngpim
   85. isnrg
   86. nrgabv
   87. nrgngp
   88. nrgring
   89. nmmul
   90. nrgdsdi
   91. nrgdsdir
   92. nm1
   93. unitnmn0
   94. nminvr
   95. nmdvr
   96. nrgdomn
   97. nrgtgp
   98. subrgnrg
   99. tngnrg
   100. isnlm
   101. nmvs
   102. nlmngp
   103. nlmlmod
   104. nlmnrg
   105. nlmngp2
   106. nlmdsdi
   107. nlmdsdir
   108. nlmmul0or
   109. sranlm
   110. nlmvscnlem2
   111. nlmvscnlem1
   112. nlmvscn
   113. rlmnlm
   114. rlmnm
   115. nrgtrg
   116. nrginvrcnlem
   117. nrginvrcn
   118. nrgtdrg
   119. nlmtlm
   120. isnvc
   121. nvcnlm
   122. nvclvec
   123. nvclmod
   124. isnvc2
   125. nvctvc
   126. lssnlm
   127. lssnvc
   128. rlmnvc
   129. 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. cnn0opn
    31. zringnrg
    32. remetdval
    33. remet
    34. rexmet
    35. bl2ioo
    36. ioo2bl
    37. ioo2blex
    38. blssioo
    39. tgioo
    40. qdensere2
    41. blcvx
    42. rehaus
    43. tgqioo
    44. re2ndc
    45. resubmet
    46. tgioo2
    47. rerest
    48. tgioo4
    49. tgioo3
    50. xrtgioo
    51. xrrest
    52. xrrest2
    53. xrsxmet
    54. xrsdsre
    55. xrsblre
    56. xrsmopn
    57. zcld
    58. recld2
    59. zcld2
    60. zdis
    61. sszcld
    62. reperflem
    63. reperf
    64. cnperf
    65. iccntr
    66. icccmplem1
    67. icccmplem2
    68. icccmplem3
    69. icccmp
    70. reconnlem1
    71. reconnlem2
    72. reconn
    73. retopconn
    74. iccconn
    75. opnreen
    76. rectbntr0
    77. xrge0gsumle
    78. xrge0tsms
    79. xrge0tsms2
    80. metdcnlem
    81. xmetdcn2
    82. xmetdcn
    83. metdcn2
    84. metdcn
    85. msdcn
    86. cnmpt1ds
    87. cnmpt2ds
    88. nmcn
    89. ngnmcncn
    90. abscn
    91. metdsval
    92. metdsf
    93. metdsge
    94. metds0
    95. metdstri
    96. metdsle
    97. metdsre
    98. metdseq0
    99. metdscnlem
    100. metdscn
    101. metdscn2
    102. metnrmlem1a
    103. metnrmlem1
    104. metnrmlem2
    105. metnrmlem3
    106. metnrm
    107. metreg
    108. addcnlem
    109. addcn
    110. subcn
    111. mulcn
    112. divcnOLD
    113. mpomulcn
    114. divcn
    115. cnfldtgp
    116. fsumcn
    117. fsum2cn
    118. expcn
    119. divccn
    120. expcnOLD
    121. divccnOLD
    122. 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. cncfcdm
    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. negcncfOLD
    50. negfcncf
    51. abscncfALT
    52. cncfcnvcn
    53. expcncf
    54. cnmptre
    55. cnmpopc
    56. iirev
    57. iirevcn
    58. iihalf1
    59. iihalf1cn
    60. iihalf1cnOLD
    61. iihalf2
    62. iihalf2cn
    63. iihalf2cnOLD
    64. elii1
    65. elii2
    66. iimulcl
    67. iimulcn
    68. iimulcnOLD
    69. icoopnst
    70. iocopnst
    71. icchmeo
    72. icchmeoOLD
    73. icopnfcnv
    74. icopnfhmeo
    75. iccpnfcnv
    76. iccpnfhmeo
    77. xrhmeo
    78. xrhmph
    79. xrcmp
    80. xrconn
    81. icccvx
    82. oprpiece1res1
    83. oprpiece1res2
    84. cnrehmeo
    85. cnrehmeoOLD
    86. cnheiborlem
    87. cnheibor
    88. cnllycmp
    89. rellycmp
    90. bndth
    91. evth
    92. evth2
    93. lebnumlem1
    94. lebnumlem2
    95. lebnumlem3
    96. lebnum
    97. xlebnum
    98. 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. reparphtiOLD
    33. reparpht
    34. 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