# mathlibdocumentation

topology.metric_space.completion

# 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

@[instance]

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

Equations
theorem metric.completion.uniform_continuous_dist {α : Type u}  :
uniform_continuous (λ (p : , dist p.fst p.snd)

The new distance is uniformly continuous.

theorem metric.completion.dist_eq {α : Type u} (x y : α) :
y = dist x y

The new distance is an extension of the original distance.

theorem metric.completion.dist_self {α : Type u} (x : uniform_space.completion α) :
dist x x = 0
theorem metric.completion.dist_comm {α : Type u} (x y : uniform_space.completion α) :
dist x y = dist y x
theorem metric.completion.dist_triangle {α : Type u} (x y z : uniform_space.completion α) :
dist x z dist x y + dist y z
theorem metric.completion.mem_uniformity_dist {α : Type u} (s : set ) :
∃ (ε : ) (H : ε > 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 metric.completion.eq_of_dist_eq_zero {α : Type u} (x y : uniform_space.completion α) (h : dist x y = 0) :
x = y

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

theorem metric.completion.uniformity_dist' {α : Type u}  :
= ⨅ (ε : {ε // 0 < ε}), 𝓟 {p : | dist p.fst p.snd < ε.val}

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

theorem metric.completion.uniformity_dist {α : Type u}  :
= ⨅ (ε : ) (H : ε > 0), 𝓟 {p : | dist p.fst p.snd < ε}
@[instance]
def metric.completion.metric_space {α : Type u}  :

Metric space structure on the completion of a pseudo_metric space.

Equations
theorem metric.completion.coe_isometry {α : Type u}  :

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