Metamath Proof Explorer


Table of Contents - 12.4.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