# 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]
def metric.has_dist {α : Type u} [metric_space α] :

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 : α) :
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 ) :
∃ (ε : ) (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} [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 α] :
= ⨅ (ε : {ε // 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} [metric_space α] :
= ⨅ (ε : ) (H : ε > 0), 𝓟 {p : | dist p.fst p.snd < ε}

@[instance]
def metric.completion.metric_space {α : Type u} [metric_space α] :

Metric space structure on the completion of a metric space.

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

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