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. nmfval2
   16. nmval2
   17. nmf2
   18. nmpropd
   19. nmpropd2
   20. isngp
   21. isngp2
   22. isngp3
   23. ngpgrp
   24. ngpms
   25. ngpxms
   26. ngptps
   27. ngpmet
   28. ngpds
   29. ngpdsr
   30. ngpds2
   31. ngpds2r
   32. ngpds3
   33. ngpds3r
   34. ngprcan
   35. ngplcan
   36. isngp4
   37. ngpinvds
   38. ngpsubcan
   39. nmf
   40. nmcl
   41. nmge0
   42. nmeq0
   43. nmne0
   44. nmrpcl
   45. nminv
   46. nmmtri
   47. nmsub
   48. nmrtri
   49. nm2dif
   50. nmtri
   51. nmtri2
   52. ngpi
   53. nm0
   54. nmgt0
   55. sgrim
   56. sgrimval
   57. subgnm
   58. subgnm2
   59. subgngp
   60. ngptgp
   61. ngppropd
   62. reldmtng
   63. tngval
   64. tnglem
   65. tngbas
   66. tngplusg
   67. tng0
   68. tngmulr
   69. tngsca
   70. tngvsca
   71. tngip
   72. tngds
   73. tngtset
   74. tngtopn
   75. tngnm
   76. tngngp2
   77. tngngpd
   78. tngngp
   79. tnggrpr
   80. tngngp3
   81. nrmtngdist
   82. nrmtngnrm
   83. tngngpim
   84. isnrg
   85. nrgabv
   86. nrgngp
   87. nrgring
   88. nmmul
   89. nrgdsdi
   90. nrgdsdir
   91. nm1
   92. unitnmn0
   93. nminvr
   94. nmdvr
   95. nrgdomn
   96. nrgtgp
   97. subrgnrg
   98. tngnrg
   99. isnlm
   100. nmvs
   101. nlmngp
   102. nlmlmod
   103. nlmnrg
   104. nlmngp2
   105. nlmdsdi
   106. nlmdsdir
   107. nlmmul0or
   108. sranlm
   109. nlmvscnlem2
   110. nlmvscnlem1
   111. nlmvscn
   112. rlmnlm
   113. rlmnm
   114. nrgtrg
   115. nrginvrcnlem
   116. nrginvrcn
   117. nrgtdrg
   118. nlmtlm
   119. isnvc
   120. nvcnlm
   121. nvclvec
   122. nvclmod
   123. isnvc2
   124. nvctvc
   125. lssnlm
   126. lssnvc
   127. rlmnvc
   128. 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. cncfmet
    35. cncfcn
    36. cncfcn1
    37. cncfmptc
    38. cncfmptid
    39. cncfmpt1f
    40. cncfmpt2f
    41. cncfmpt2ss
    42. addccncf
    43. cdivcncf
    44. negcncf
    45. negfcncf
    46. abscncfALT
    47. cncfcnvcn
    48. expcncf
    49. cnmptre
    50. cnmpopc
    51. iirev
    52. iirevcn
    53. iihalf1
    54. iihalf1cn
    55. iihalf2
    56. iihalf2cn
    57. elii1
    58. elii2
    59. iimulcl
    60. iimulcn
    61. icoopnst
    62. iocopnst
    63. icchmeo
    64. icopnfcnv
    65. icopnfhmeo
    66. iccpnfcnv
    67. iccpnfhmeo
    68. xrhmeo
    69. xrhmph
    70. xrcmp
    71. xrconn
    72. icccvx
    73. oprpiece1res1
    74. oprpiece1res2
    75. cnrehmeo
    76. cnheiborlem
    77. cnheibor
    78. cnllycmp
    79. rellycmp
    80. bndth
    81. evth
    82. evth2
    83. lebnumlem1
    84. lebnumlem2
    85. lebnumlem3
    86. lebnum
    87. xlebnum
    88. 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