Documentation

Mathlib.Topology.MetricSpace.Basic

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 {α : 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
      @[instance 100]
      instance MetricSpace.instT0Space {γ : Type w} [MetricSpace γ] :
      Equations
      • =
      theorem Metric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] {f : γβ} :
      UniformEmbedding f (ε > 0, δ > 0, ∀ {a b : γ}, dist a b < δdist (f a) (f b) < ε) δ > 0, ε > 0, ∀ {a b : γ}, dist (f a) (f b) < εdist a b < δ

      A map between metric spaces is a uniform embedding if and only if the distance between f x and f y is controlled in terms of the distance between x and y and conversely.

      @[reducible, inline]

      If a PseudoMetricSpace is a T₀ space, then it is a MetricSpace.

      Equations
      Instances For
        @[instance 100]

        A metric space induces an emetric space

        Equations
        theorem Metric.isClosed_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {s : Set γ} {ε : } (hε : 0 < ε) (hs : s.Pairwise fun (x y : γ) => ε dist x y) :
        theorem Metric.closedEmbedding_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {α : Type u_3} [TopologicalSpace α] [DiscreteTopology α] {ε : } (hε : 0 < ε) {f : αγ} (hf : Pairwise fun (x y : α) => ε dist (f x) (f y)) :
        theorem Metric.uniformEmbedding_bot_of_pairwise_le_dist {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {ε : } (hε : 0 < ε) {f : βα} (hf : Pairwise fun (x y : β) => ε dist (f x) (f y)) :

        If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

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

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

          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 EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : αα) (edist_ne_top : ∀ (x y : α), edist x y ) (h : ∀ (x y : α), dist x y = (edist x y).toReal) :

            One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals.

            Equations
            Instances For
              def EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ (x y : α), edist x y ) :

              One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space.

              Equations
              Instances For

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

                Equations
                • m.replaceBornology H = let __src := MetricSpace.toPseudoMetricSpace.replaceBornology H; MetricSpace.mk
                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
                  @[reducible, inline]
                  abbrev MetricSpace.induced {γ : Type u_3} {β : Type u_4} (f : γβ) (hf : Function.Injective f) (m : MetricSpace β) :

                  Metric space structure pulled back by an injective function. Injectivity is necessary to ensure that dist x y = 0 only if x = y.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev UniformEmbedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : MetricSpace β] (f : αβ) (h : UniformEmbedding f) :

                    Pull back a metric space structure by a uniform embedding. This is a version of MetricSpace.induced useful in case if the domain already has a UniformSpace structure.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Embedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : MetricSpace β] (f : αβ) (h : Embedding f) :

                      Pull back a metric space structure by an embedding. This is a version of MetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

                      Equations
                      Instances For
                        instance Subtype.metricSpace {α : Type u_3} {p : αProp} [MetricSpace α] :
                        Equations
                        Equations
                        Equations

                        Instantiate the reals as a metric space.

                        Equations
                        Equations
                        instance Prod.metricSpaceMax {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] :
                        MetricSpace (γ × β)
                        Equations
                        instance metricSpacePi {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → MetricSpace (π b)] :
                        MetricSpace ((b : β) → π b)

                        A finite product of metric spaces is a metric space, with the sup distance.

                        Equations
                        theorem Metric.secondCountable_of_countable_discretization {α : Type u} [MetricSpace α] (H : ε > 0, ∃ (β : Type u_3) (x : Encodable β) (F : αβ), ∀ (x y : α), F x = F ydist x y ε) :

                        A metric space is second countable if one can reconstruct up to any ε>0 any element of the space from countably many data.

                        Equations
                        Equations

                        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
                        Equations
                        • instPseudoMetricSpaceAdditive_1 = inst
                        Equations
                        • instPseudoMetricSpaceMultiplicative_1 = inst
                        @[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
                        Equations

                        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