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. 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