doc: provide an actual docstring to MetricSpace (#23123)

Docstrings which assume you are reading them from the file they are defined in are completely useless on hover.

Author: YaelDillies

Mathlib/Topology/EMetricSpace/Defs.lean

@@ -59,21 +59,22 @@ def uniformSpaceOfEDist (edist : α → α → ℝ≥0∞) (edist_self : ∀ x :
     ⟨ε / 2, ENNReal.half_pos ε0.ne', fun _ h₁ _ h₂ =>
       (ENNReal.add_lt_add h₁ h₂).trans_eq (ENNReal.add_halves _)⟩
 
--- the uniform structure is embedded in the emetric space structure
--- to avoid instance diamond issues. See Note [forgetful inheritance].
-/-- Extended (pseudo) metric spaces, with an extended distance `edist` possibly taking the
-value ∞
-
-Each pseudo_emetric space induces a canonical `UniformSpace` and hence a canonical
-`TopologicalSpace`.
-This is enforced in the type class definition, by extending the `UniformSpace` structure. When
-instantiating a `PseudoEMetricSpace` structure, the uniformity fields are not necessary, they
-will be filled in by default. There is a default value for the uniformity, that can be substituted
-in cases of interest, for instance when instantiating a `PseudoEMetricSpace` structure
-on a product.
-
-Continuity of `edist` is proved in `Topology.Instances.ENNReal`
--/
+/-- A pseudo extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist`
+satisfying reflexivity `edist x x = 0`, commutativity `edist x y = edist y x`, and the triangle
+inequality `edist x z ≤ edist x y + edist y z`.
+
+Note that we do not require `edist x y = 0 → x = y`. See extended metric spaces (`EMetricSpace`) for
+the similar class with that stronger assumption.
+
+Any pseudo extended metric space is a topological space and a uniform space (see `TopologicalSpace`,
+`UniformSpace`), where the topology and uniformity come from the metric.
+Note that a T1 pseudo extended metric space is just an extended metric space.
+
+We make the uniformity/topology part of the data instead of deriving it from the metric. This eg
+ensures that we do not get a diamond when doing
+`[PseudoEMetricSpace α] [PseudoEMetricSpace β] : TopologicalSpace (α × β)`:
+The product metric and product topology agree, but not definitionally so.
+See Note [forgetful inheritance]. -/
 class PseudoEMetricSpace (α : Type u) : Type u extends EDist α  where
   edist_self : ∀ x : α, edist x x = 0
   edist_comm : ∀ x y : α, edist x y = edist y x
@@ -538,8 +539,21 @@ end Compact
 
 end EMetric
 
---namespace
-/-- We now define `EMetricSpace`, extending `PseudoEMetricSpace`. -/
+/-- An extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist` satisfying
+`edist x y = 0 ↔ x = y`, commutativity `edist x y = edist y x`, and the triangle inequality
+`edist x z ≤ edist x y + edist y z`.
+
+See pseudo extended metric spaces (`PseudoEMetricSpace`) for the similar class with the
+`edist x y = 0 ↔ x = y` assumption weakened to `edist x x = 0`.
+
+Any extended metric space is a T1 topological space and a uniform space (see `TopologicalSpace`,
+`T1Space`, `UniformSpace`), where the topology and uniformity come from the metric.
+
+We make the uniformity/topology part of the data instead of deriving it from the metric.
+This eg ensures that we do not get a diamond when doing
+`[EMetricSpace α] [EMetricSpace β] : TopologicalSpace (α × β)`:
+The product metric and product topology agree, but not definitionally so.
+See Note [forgetful inheritance]. -/
 class EMetricSpace (α : Type u) : Type u extends PseudoEMetricSpace α where
   eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
 

Mathlib/Topology/MetricSpace/Defs.lean

@@ -35,7 +35,21 @@ universe u v w
 variable {α : Type u} {β : Type v} {X ι : Type*}
 variable [PseudoMetricSpace α]
 
-/-- We now define `MetricSpace`, extending `PseudoMetricSpace`. -/
+/-- A metric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
+`dist x y = 0 ↔ x = y`, commutativity `dist x y = dist y x`, and the triangle inequality
+`dist x z ≤ dist x y + dist y z`.
+
+See pseudometric spaces (`PseudoMetricSpace`) for the similar class with the `dist x y = 0 ↔ x = y`
+assumption weakened to `dist x x = 0`.
+
+Any metric space is a T1 topological space and a uniform space (see `TopologicalSpace`, `T1Space`,
+`UniformSpace`), where the topology and uniformity come from the metric.
+
+We make the uniformity/topology part of the data instead of deriving it from the metric.
+This eg ensures that we do not get a diamond when doing
+`[MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β)`:
+The product metric and product topology agree, but not definitionally so.
+See Note [forgetful inheritance]. -/
 class MetricSpace (α : Type u) : Type u extends PseudoMetricSpace α where
   eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y
 

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -99,16 +99,22 @@ private theorem dist_nonneg' {α} {x y : α} (dist : α → α → ℝ)
     _ = 2 * dist x y := by rw [two_mul, dist_comm]
   nonneg_of_mul_nonneg_right this two_pos
 
-/-- Pseudo metric and Metric spaces
-
-A pseudo metric space is endowed with a distance for which the requirement `d(x,y)=0 → x = y` might
-not hold. A metric space is a pseudo metric space such that `d(x,y)=0 → x = y`.
-Each pseudo metric space induces a canonical `UniformSpace` and hence a canonical
-`TopologicalSpace` This is enforced in the type class definition, by extending the `UniformSpace`
-structure. When instantiating a `PseudoMetricSpace` structure, the uniformity fields are not
-necessary, they will be filled in by default. In the same way, each (pseudo) metric space induces a
-(pseudo) emetric space structure. It is included in the structure, but filled in by default.
--/
+/-- A pseudometric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
+reflexivity `dist x x = 0`, commutativity `dist x y = dist y x`, and the triangle inequality
+`dist x z ≤ dist x y + dist y z`.
+
+Note that we do not require `dist x y = 0 → x = y`. See metric spaces (`MetricSpace`) for the
+similar class with that stronger assumption.
+
+Any pseudometric space is a topological space and a uniform space (see `TopologicalSpace`,
+`UniformSpace`), where the topology and uniformity come from the metric.
+Note that a T1 pseudometric space is just a metric space.
+
+We make the uniformity/topology part of the data instead of deriving it from the metric. This eg
+ensures that we do not get a diamond when doing
+`[PseudoMetricSpace α] [PseudoMetricSpace β] : TopologicalSpace (α × β)`:
+The product metric and product topology agree, but not definitionally so.
+See Note [forgetful inheritance]. -/
 class PseudoMetricSpace (α : Type u) : Type u extends Dist α where
   dist_self : ∀ x : α, dist x x = 0
   dist_comm : ∀ x y : α, dist x y = dist y x