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

source

class MetricSpace (α : Type u) extends PseudoMetricSpace :

Type u

We now define MetricSpace, extending PseudoMetricSpace.

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
edist : α → α → ENNReal
edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y

Instances

source

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.

source

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 ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : α), dist x y < ε → y ∈ s) (eq_of_dist_eq_zero : ∀ (x y : α), dist x y = 0 → x = y) :

MetricSpace α

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

MetricSpace.ofDistTopology dist dist_self dist_comm dist_triangle H eq_of_dist_eq_zero = let __src := PseudoMetricSpace.ofDistTopology dist dist_self dist_comm dist_triangle H; MetricSpace.mk ⋯

Instances For

source

theorem eq_of_dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

dist x y = 0 → x = y

source

@[simp]

theorem dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

dist x y = 0 ↔ x = y

source

@[simp]

theorem zero_eq_dist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

0 = dist x y ↔ x = y

source

theorem dist_ne_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

dist x y ≠ 0 ↔ x ≠ y

source

@[simp]

theorem dist_le_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

dist x y ≤ 0 ↔ x = y

source

@[simp]

theorem dist_pos {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

0 < dist x y ↔ x ≠ y

source

theorem eq_of_forall_dist_le {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} (h : ∀ ε > 0, dist x y ≤ ε) :

x = y

source

theorem eq_of_nndist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

nndist x y = 0 → x = y

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

source

@[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

source

@[simp]

theorem zero_eq_nndist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} :

0 = nndist x y ↔ x = y

source

@[simp]

theorem Metric.closedBall_zero {γ : Type w} [MetricSpace γ] {x : γ} :

Metric.closedBall x 0 = {x}

source

@[simp]

theorem Metric.sphere_zero {γ : Type w} [MetricSpace γ] {x : γ} :

Metric.sphere x 0 = {x}

source

theorem Metric.subsingleton_closedBall {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) :

Set.Subsingleton (Metric.closedBall x r)

source

theorem Metric.subsingleton_sphere {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) :

Set.Subsingleton (Metric.sphere x r)

source

instance MetricSpace.instT0Space {γ : Type w} [MetricSpace γ] :

T0Space γ

Equations

⋯ = ⋯

source

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.

source

@[reducible]

def MetricSpace.ofT0PseudoMetricSpace (α : Type u_3) [PseudoMetricSpace α] [T0Space α] :

MetricSpace α

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

Equations

MetricSpace.ofT0PseudoMetricSpace α = MetricSpace.mk ⋯

Instances For

source

instance MetricSpace.toEMetricSpace {γ : Type w} [MetricSpace γ] :

EMetricSpace γ

A metric space induces an emetric space

Equations

MetricSpace.toEMetricSpace = EMetricSpace.ofT0PseudoEMetricSpace γ

source

theorem Metric.isClosed_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {s : Set γ} {ε : ℝ} (hε : 0 < ε) (hs : Set.Pairwise s fun (x y : γ) => ε ≤ dist x y) :

IsClosed s

source

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

ClosedEmbedding f

source

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

UniformEmbedding f

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

source

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

MetricSpace γ

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

MetricSpace.replaceUniformity m H = MetricSpace.mk ⋯

Instances For

source

theorem MetricSpace.replaceUniformity_eq {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ) :

MetricSpace.replaceUniformity m H = m

source

@[reducible]

def MetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :

MetricSpace γ

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

MetricSpace.replaceTopology m H = MetricSpace.replaceUniformity m ⋯

Instances For

source

theorem MetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :

MetricSpace.replaceTopology m H = m

source

@[reducible]

def EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (x y : α), dist x y = (edist x y).toReal) :

MetricSpace α

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

EMetricSpace.toMetricSpaceOfDist dist edist_ne_top h = MetricSpace.ofT0PseudoMetricSpace α

Instances For

source

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

MetricSpace α

Equations

EMetricSpace.toMetricSpace h = EMetricSpace.toMetricSpaceOfDist (fun (x y : α) => (edist x y).toReal) h ⋯

Instances For

source

def MetricSpace.replaceBornology {α : Type u_3} [B : Bornology α] (m : MetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) :

MetricSpace α

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

MetricSpace.replaceBornology m H = let __src := PseudoMetricSpace.replaceBornology MetricSpace.toPseudoMetricSpace H; MetricSpace.mk ⋯

Instances For

source

theorem MetricSpace.replaceBornology_eq {α : Type u_3} [m : MetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) :

MetricSpace.replaceBornology m H = m

source

@[reducible]

def MetricSpace.induced {γ : Type u_3} {β : Type u_4} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) :

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

MetricSpace.induced f hf m = let __src := PseudoMetricSpace.induced f MetricSpace.toPseudoMetricSpace; MetricSpace.mk ⋯

Instances For

source

@[reducible]

def UniformEmbedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : UniformEmbedding f) :

MetricSpace α

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

UniformEmbedding.comapMetricSpace f h = MetricSpace.replaceUniformity (MetricSpace.induced f ⋯ m) ⋯

Instances For

source

@[reducible]

def Embedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : Embedding f) :

MetricSpace α

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