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.eq_of_dist_eq_zero {α : Type u} [self : MetricSpace α] {x : α} {y : α} :

dist x y = 0 → x = y

source

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

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

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

(Metric.closedBall x r).Subsingleton

source

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

(Metric.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 = MetricSpace.mk ⋯

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