mathlib documentation

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

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.