# The completion of a metric space #

Completion of uniform spaces are already defined in Topology.UniformSpace.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

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

Equations
• UniformSpace.Completion.instDist = { dist := }

The new distance is uniformly continuous.

theorem UniformSpace.Completion.continuous_dist {α : Type u} {β : Type v} [] {f : } {g : } (hf : ) (hg : ) :
Continuous fun (x : β) => dist (f x) (g x)

The new distance is continuous.

@[simp]
theorem UniformSpace.Completion.dist_eq {α : Type u} (x : α) (y : α) :
dist (α x) (α y) = dist x y

The new distance is an extension of the original distance.

theorem UniformSpace.Completion.dist_self {α : Type u} (x : ) :
dist x x = 0
theorem UniformSpace.Completion.dist_comm {α : Type u} (x : ) (y : ) :
dist x y = dist y x
theorem UniformSpace.Completion.dist_triangle {α : Type u} (x : ) (y : ) (z : ) :
dist x z dist x y + dist y z
theorem UniformSpace.Completion.mem_uniformity_dist {α : Type u} (s : ) :
ε > 0, ∀ {a b : }, dist a b < ε(a, b) s

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

theorem UniformSpace.Completion.uniformity_dist' {α : Type u} :
= ⨅ (ε : { ε : // 0 < ε }), Filter.principal {p : | dist p.1 p.2 < ε}

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

theorem UniformSpace.Completion.uniformity_dist {α : Type u} :
= ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : | dist p.1 p.2 < ε}

Metric space structure on the completion of a pseudo_metric space.

Equations
• UniformSpace.Completion.instMetricSpace =
@[deprecated eq_of_dist_eq_zero]
theorem UniformSpace.Completion.eq_of_dist_eq_zero {α : Type u} (x : ) (y : ) (h : dist x y = 0) :
x = y

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

@[simp]
theorem UniformSpace.Completion.edist_eq {α : Type u} (x : α) (y : α) :
edist (α x) (α y) = edist x y
theorem LipschitzWith.completion_extension {α : Type u} {β : Type v} [] [] {f : αβ} {K : NNReal} (h : ) :
theorem LipschitzWith.completion_map {α : Type u} {β : Type v} {f : αβ} {K : NNReal} (h : ) :
theorem Isometry.completion_extension {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :
theorem Isometry.completion_map {α : Type u} {β : Type v} {f : αβ} (h : ) :