mathlib3 documentation

topology.metric_space.completion

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.

Equations
@[protected]

The new distance is uniformly continuous.

@[protected]
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.

@[protected]

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

@[protected]

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

@[protected]

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]