# 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 :

We now define MetricSpace, extending PseudoMetricSpace.

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

Two metric space structures with the same distance coincide.

def MetricSpace.ofDistTopology {α : Type u} [] (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 α), 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} [] {x : γ} {y : γ} :
dist x y = 0x = y
@[simp]
theorem dist_eq_zero {γ : Type w} [] {x : γ} {y : γ} :
dist x y = 0 x = y
@[simp]
theorem zero_eq_dist {γ : Type w} [] {x : γ} {y : γ} :
0 = dist x y x = y
theorem dist_ne_zero {γ : Type w} [] {x : γ} {y : γ} :
dist x y 0 x y
@[simp]
theorem dist_le_zero {γ : Type w} [] {x : γ} {y : γ} :
dist x y 0 x = y
@[simp]
theorem dist_pos {γ : Type w} [] {x : γ} {y : γ} :
0 < dist x y x y
theorem eq_of_forall_dist_le {γ : Type w} [] {x : γ} {y : γ} (h : ε > 0, dist x y ε) :
x = y
theorem eq_of_nndist_eq_zero {γ : Type w} [] {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} [] {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} [] {x : γ} {y : γ} :
0 = nndist x y x = y
@[simp]
theorem Metric.closedBall_zero {γ : Type w} [] {x : γ} :
= {x}
@[simp]
theorem Metric.sphere_zero {γ : Type w} [] {x : γ} :
= {x}
theorem Metric.subsingleton_closedBall {γ : Type w} [] (x : γ) {r : } (hr : r 0) :
.Subsingleton
theorem Metric.subsingleton_sphere {γ : Type w} [] (x : γ) {r : } (hr : r 0) :
(Metric.sphere x r).Subsingleton
@[instance 100]
instance MetricSpace.instT0Space {γ : Type w} [] :
Equations
• =
theorem Metric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [] [] {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]
instance MetricSpace.toEMetricSpace {γ : Type w} [] :

A metric space induces an emetric space

Equations
• MetricSpace.toEMetricSpace =
theorem Metric.isClosed_of_pairwise_le_dist {γ : Type w} [] {s : Set γ} {ε : } (hε : 0 < ε) (hs : s.Pairwise fun (x y : γ) => ε dist x y) :
theorem Metric.closedEmbedding_of_pairwise_le_dist {γ : Type w} [] {α : Type u_3} [] [] {ε : } (hε : 0 < ε) {f : αγ} (hf : Pairwise fun (x y : α) => ε dist (f x) (f y)) :
theorem Metric.uniformEmbedding_bot_of_pairwise_le_dist {α : Type u} {β : 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 β.

def MetricSpace.replaceUniformity {γ : Type u_3} [U : ] (m : ) (H : ) :

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
• m.replaceUniformity H =
Instances For
theorem MetricSpace.replaceUniformity_eq {γ : Type u_3} [U : ] (m : ) (H : ) :
m.replaceUniformity H = m
@[reducible, inline]
abbrev MetricSpace.replaceTopology {γ : Type u_3} [U : ] (m : ) (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 : ] (m : ) (H : U = UniformSpace.toTopologicalSpace) :
m.replaceTopology H = m
@[reducible, inline]
abbrev EMetricSpace.toMetricSpaceOfDist {α : Type u} [] (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} [] (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
def MetricSpace.replaceBornology {α : Type u_3} [B : ] (m : ) (H : ∀ (s : Set α), ) :

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;
Instances For
theorem MetricSpace.replaceBornology_eq {α : Type u_3} [m : ] [B : ] (H : ∀ (s : Set α), ) :
m.replaceBornology H = m
@[reducible, inline]
abbrev MetricSpace.induced {γ : Type u_3} {β : Type u_4} (f : γβ) (hf : ) (m : ) :

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} [] [m : ] (f : αβ) (h : ) :

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} [] [m : ] (f : αβ) (h : ) :

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} [] :
Equations
instance instMetricSpaceAddOpposite {α : Type u_3} [] :
Equations
instance instMetricSpaceMulOpposite {α : Type u_3} [] :
Equations
Equations
Equations
instance Real.metricSpace :

Instantiate the reals as a metric space.

Equations
Equations
instance instMetricSpaceULift {β : Type v} [] :
Equations
instance Prod.metricSpaceMax {β : Type v} {γ : Type w} [] [] :
MetricSpace (γ × β)
Equations
• Prod.metricSpaceMax =
instance metricSpacePi {β : Type v} {π : βType u_3} [] [(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} [] (H : ε > 0, ∃ (β : Type u_3) (x : ) (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.

instance SeparationQuotient.instDist {α : Type u} :
Equations
• SeparationQuotient.instDist = { dist := }
theorem SeparationQuotient.dist_mk {α : Type u} (p : α) (q : α) :
= dist p q
Equations
• SeparationQuotient.instMetricSpace =

### 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 : ) (b : ) :
dist (Additive.toMul a) (Additive.toMul b) = dist a b
@[simp]
theorem dist_toAdd {X : Type u_1} [Dist X] (a : ) (b : ) :
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} (a : X) (b : X) :
nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
@[simp]
theorem nndist_ofAdd {X : Type u_1} (a : X) (b : X) :
nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
@[simp]
theorem nndist_toMul {X : Type u_1} (a : ) (b : ) :
nndist (Additive.toMul a) (Additive.toMul b) = nndist a b
@[simp]
theorem nndist_toAdd {X : Type u_1} (a : ) (b : ) :
nndist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = nndist a b
instance instMetricSpaceAdditive {X : Type u_1} [] :
Equations
• instMetricSpaceAdditive = inst
instance instMetricSpaceMultiplicative {X : Type u_1} [] :
Equations
• instMetricSpaceMultiplicative = inst
instance MulOpposite.instMetricSpace {X : Type u_1} [] :
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} (a : X) (b : X) :
nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
@[simp]
theorem nndist_ofDual {X : Type u_1} (a : Xᵒᵈ) (b : Xᵒᵈ) :
nndist (OrderDual.ofDual a) (OrderDual.ofDual b) = nndist a b
instance instMetricSpaceOrderDual {X : Type u_1} [] :
Equations
• instMetricSpaceOrderDual = inst