# 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

@[protected, instance]
noncomputable def uniform_space.completion.has_dist {α : Type u}  :

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

Equations
@[protected]

The new distance is uniformly continuous.

@[protected]
theorem uniform_space.completion.continuous_dist {α : Type u} {β : Type v} {f g : β → } (hf : continuous f) (hg : continuous g) :
continuous (λ (x : β), has_dist.dist (f x) (g x))

The new distance is continuous.

@[protected, simp]
theorem uniform_space.completion.dist_eq {α : Type u} (x y : α) :
=

The new distance is an extension of the original distance.

@[protected]
theorem uniform_space.completion.dist_self {α : Type u} (x : uniform_space.completion α) :
= 0
@[protected]
theorem uniform_space.completion.dist_comm {α : Type u} (x y : uniform_space.completion α) :
=
@[protected]
@[protected]
theorem uniform_space.completion.mem_uniformity_dist {α : Type u} (s : set ) :
∃ (ε : ) (H : ε > 0), ∀ {a b : , < ε(a, b) s

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

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

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

@[protected]
theorem uniform_space.completion.uniformity_dist' {α : Type u}  :
= ⨅ (ε : {ε // 0 < ε}), filter.principal {p : | p.snd < ε.val}

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

@[protected]
theorem uniform_space.completion.uniformity_dist {α : Type u}  :
= ⨅ (ε : ) (H : ε > 0), filter.principal {p : | p.snd < ε}
@[protected, instance]
noncomputable def uniform_space.completion.metric_space {α : Type u}  :

Metric space structure on the completion of a pseudo_metric space.

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

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

@[protected, simp]
theorem uniform_space.completion.edist_eq {α : Type u} (x y : α) :