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