mathlib documentation


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


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


The new distance is uniformly continuous.

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.

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

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

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

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.

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

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

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

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

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