Documentation

Mathlib.Topology.MetricSpace.Defs

Metric spaces #

This file defines metric spaces and shows some of their basic properties.

Many definitions and theorems expected on metric spaces are already introduced on uniform spaces and topological spaces. This includes open and closed sets, compactness, completeness, continuity and uniform continuity.

TODO (anyone): Add "Main results" section.

Implementation notes #

A lot of elementary properties don't require eq_of_dist_eq_zero, hence are stated and proven for PseudoMetricSpaces in PseudoMetric.lean.

Tags #

metric, pseudo_metric, dist

class MetricSpace (α : Type u) extends PseudoMetricSpace :

We now define MetricSpace, extending PseudoMetricSpace.

Instances
    theorem MetricSpace.eq_of_dist_eq_zero {α : Type u} [self : MetricSpace α] {x : α} {y : α} :
    dist x y = 0x = y
    theorem MetricSpace.ext_iff {α : Type u_3} {m : MetricSpace α} {m' : MetricSpace α} :
    m = m' PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
    theorem MetricSpace.ext {α : Type u_3} {m : MetricSpace α} {m' : MetricSpace α} (h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist) :
    m = m'

    Two metric space structures with the same distance coincide.

    def MetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : αα) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z) (H : ∀ (s : Set α), IsOpen s xs, ε > 0, ∀ (y : α), dist x y < εy s) (eq_of_dist_eq_zero : ∀ (x y : α), dist x y = 0x = y) :

    Construct a metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.

    Equations
    Instances For
      theorem eq_of_dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      dist x y = 0x = y
      @[simp]
      theorem dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      dist x y = 0 x = y
      @[simp]
      theorem zero_eq_dist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      0 = dist x y x = y
      theorem dist_ne_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      dist x y 0 x y
      @[simp]
      theorem dist_le_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      dist x y 0 x = y
      @[simp]
      theorem dist_pos {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      0 < dist x y x y
      theorem eq_of_forall_dist_le {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} (h : ε > 0, dist x y ε) :
      x = y
      theorem eq_of_nndist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      nndist x y = 0x = y

      Deduce the equality of points from the vanishing of the nonnegative distance

      @[simp]
      theorem nndist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      nndist x y = 0 x = y

      Characterize the equality of points as the vanishing of the nonnegative distance

      @[simp]
      theorem zero_eq_nndist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :
      0 = nndist x y x = y
      @[simp]
      theorem Metric.closedBall_zero {γ : Type w} [MetricSpace γ] {x : γ} :
      @[simp]
      theorem Metric.sphere_zero {γ : Type w} [MetricSpace γ] {x : γ} :
      theorem Metric.subsingleton_closedBall {γ : Type w} [MetricSpace γ] (x : γ) {r : } (hr : r 0) :
      (Metric.closedBall x r).Subsingleton
      theorem Metric.subsingleton_sphere {γ : Type w} [MetricSpace γ] (x : γ) {r : } (hr : r 0) :
      (Metric.sphere x r).Subsingleton
      @[reducible, inline]
      abbrev MetricSpace.replaceUniformity {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ) :

      Build a new metric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance]. See Note [reducible non-instances].

      Equations
      Instances For
        theorem MetricSpace.replaceUniformity_eq {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ) :
        m.replaceUniformity H = m
        @[reducible, inline]
        abbrev MetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :

        Build a new metric space from an old one where the bundled topological structure is provably (but typically non-definitionaly) equal to some given topological structure. See Note [forgetful inheritance]. See Note [reducible non-instances].

        Equations
        • m.replaceTopology H = m.replaceUniformity
        Instances For
          theorem MetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :
          m.replaceTopology H = m
          @[reducible, inline]
          abbrev MetricSpace.replaceBornology {α : Type u_3} [B : Bornology α] (m : MetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s Bornology.IsBounded s) :

          Build a new metric space from an old one where the bundled bornology structure is provably (but typically non-definitionaly) equal to some given bornology structure. See Note [forgetful inheritance]. See Note [reducible non-instances].

          Equations
          Instances For
            theorem MetricSpace.replaceBornology_eq {α : Type u_3} [m : MetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s Bornology.IsBounded s) :
            m.replaceBornology H = m

            Additive, Multiplicative #

            The distance on those type synonyms is inherited without change.

            instance instDistAdditive {X : Type u_1} [Dist X] :
            Equations
            • instDistAdditive = inst
            instance instDistMultiplicative {X : Type u_1} [Dist X] :
            Equations
            • instDistMultiplicative = inst
            @[simp]
            theorem dist_ofMul {X : Type u_1} [Dist X] (a : X) (b : X) :
            dist (Additive.ofMul a) (Additive.ofMul b) = dist a b
            @[simp]
            theorem dist_ofAdd {X : Type u_1} [Dist X] (a : X) (b : X) :
            dist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = dist a b
            @[simp]
            theorem dist_toMul {X : Type u_1} [Dist X] (a : Additive X) (b : Additive X) :
            dist (Additive.toMul a) (Additive.toMul b) = dist a b
            @[simp]
            theorem dist_toAdd {X : Type u_1} [Dist X] (a : Multiplicative X) (b : Multiplicative X) :
            dist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = dist a b
            @[simp]
            theorem nndist_ofMul {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) :
            nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
            @[simp]
            theorem nndist_ofAdd {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) :
            nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
            @[simp]
            theorem nndist_toMul {X : Type u_1} [PseudoMetricSpace X] (a : Additive X) (b : Additive X) :
            nndist (Additive.toMul a) (Additive.toMul b) = nndist a b
            @[simp]
            theorem nndist_toAdd {X : Type u_1} [PseudoMetricSpace X] (a : Multiplicative X) (b : Multiplicative X) :
            nndist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = nndist a b
            Equations
            • instMetricSpaceAdditive = inst
            Equations
            • instMetricSpaceMultiplicative = inst

            Order dual #

            The distance on this type synonym is inherited without change.

            instance instDistOrderDual {X : Type u_1} [Dist X] :
            Equations
            • instDistOrderDual = inst
            @[simp]
            theorem dist_toDual {X : Type u_1} [Dist X] (a : X) (b : X) :
            dist (OrderDual.toDual a) (OrderDual.toDual b) = dist a b
            @[simp]
            theorem dist_ofDual {X : Type u_1} [Dist X] (a : Xᵒᵈ) (b : Xᵒᵈ) :
            dist (OrderDual.ofDual a) (OrderDual.ofDual b) = dist a b
            Equations
            • instPseudoMetricSpaceOrderDual_1 = inst
            @[simp]
            theorem nndist_toDual {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) :
            nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
            @[simp]
            theorem nndist_ofDual {X : Type u_1} [PseudoMetricSpace X] (a : Xᵒᵈ) (b : Xᵒᵈ) :
            nndist (OrderDual.ofDual a) (OrderDual.ofDual b) = nndist a b
            Equations
            • instMetricSpaceOrderDual = inst