The completion of a metric space

Completion of uniform spaces are already defined in topology.uniform_space.completion. We show here that the uniform space completion of a metric space inherits a metric space structure, by extending the distance to the completion and checking that it is indeed a distance, and that it defines the same uniformity as the already defined uniform structure on the completion

source

@[instance]

def metric.has_dist {α : Type u} [metric_space α] :

has_dist (uniform_space.completion α)

The distance on the completion is obtained by extending the distance on the original space, by uniform continuity.

Equations

metric.has_dist = {dist := uniform_space.completion.extension₂ dist}

source

theorem metric.completion.uniform_continuous_dist {α : Type u} [metric_space α] :

uniform_continuous (λ (p : uniform_space.completion α × uniform_space.completion α), dist p.fst p.snd)

The new distance is uniformly continuous.

source

theorem metric.completion.dist_eq {α : Type u} [metric_space α] (x y : α) :

dist ↑x ↑y = dist x y

The new distance is an extension of the original distance.

source

theorem metric.completion.dist_self {α : Type u} [metric_space α] (x : uniform_space.completion α) :

dist x x = 0

source

theorem metric.completion.dist_comm {α : Type u} [metric_space α] (x y : uniform_space.completion α) :

dist x y = dist y x

source

theorem metric.completion.dist_triangle {α : Type u} [metric_space α] (x y z : uniform_space.completion α) :

dist x z ≤ dist x y + dist y z

source

theorem metric.completion.mem_uniformity_dist {α : Type u} [metric_space α] (s : set (uniform_space.completion α × uniform_space.completion α)) :

s ∈ 𝓤 (uniform_space.completion α) ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ {a b : uniform_space.completion α}, dist a b < ε → (a, b) ∈ s

Elements of the uniformity (defined generally for completions) can be characterized in terms of the distance.

source

theorem metric.completion.eq_of_dist_eq_zero {α : Type u} [metric_space α] (x y : uniform_space.completion α) (h : dist x y = 0) :

x = y

If two points are at distance 0, then they coincide.

source

theorem metric.completion.uniformity_dist' {α : Type u} [metric_space α] :

𝓤 (uniform_space.completion α) = ⨅ (ε : {ε // 0 < ε}), 𝓟 {p : uniform_space.completion α × uniform_space.completion α | dist p.fst p.snd < ε.val}

Reformulate completion.mem_uniformity_dist in terms that are suitable for the definition of the metric space structure.

source

theorem metric.completion.uniformity_dist {α : Type u} [metric_space α] :

𝓤 (uniform_space.completion α) = ⨅ (ε : ℝ) (H : ε > 0), 𝓟 {p : uniform_space.completion α × uniform_space.completion α | dist p.fst p.snd < ε}

source

@[instance]

def metric.completion.metric_space {α : Type u} [metric_space α] :

metric_space (uniform_space.completion α)

Metric space structure on the completion of a metric space.

Equations

metric.completion.metric_space = {to_has_dist := metric.has_dist _inst_1, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : uniform_space.completion α), ennreal.of_real (uniform_space.completion.extension₂ dist x y), edist_dist := _, to_uniform_space := uniform_space.completion.uniform_space α metric_space.to_uniform_space', uniformity_dist := _}

source

theorem metric.completion.coe_isometry {α : Type u} [metric_space α] :

isometry coe

The embedding of a metric space in its completion is an isometry.