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