mathlib3 documentation


The completion of a metric space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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 uniform_space.completion.continuous_dist {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f g : β uniform_space.completion α} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : β), has_dist.dist (f x) (g x))

The new distance is continuous.

@[protected, simp]

The new distance is an extension of the original distance.


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


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


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.

@[protected, simp]