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

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

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 : α) : 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 m' : MetricSpace α} (h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist) :

m = m'

Two metric space structures with the same distance coincide.

source

theorem MetricSpace.ext_iff {α : Type u_3} {m m' : MetricSpace α} :

m = m' ↔ PseudoMetricSpace.toDist = PseudoMetricSpace.toDist

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

One or more equations did not get rendered due to their size.

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 : γ} :

closedBall x 0 = {x}

source

@[simp]

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

sphere x 0 = {x}

source

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

(closedBall x r).Subsingleton

source

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

(sphere x r).Subsingleton

source

@[reducible, inline]

abbrev 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]. See Note [reducible non-instances].

Equations

m.replaceUniformity H = { toPseudoMetricSpace := MetricSpace.toPseudoMetricSpace.replaceUniformity H, eq_of_dist_eq_zero := ⋯ }

Instances For

source

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

m.replaceUniformity H = m

source

@[reducible, inline]

abbrev 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]. See Note [reducible non-instances].

Equations

m.replaceTopology H = m.replaceUniformity ⋯

Instances For

source

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

m.replaceTopology H = m

source

@[reducible, inline]

abbrev 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]. See Note [reducible non-instances].

Equations