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.
Equations
The new distance is uniformly continuous.
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.
Metric space structure on the completion of a metric space.
Equations
- metric.completion.metric_space = {to_has_dist := metric.has_dist _inst_1, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : uniform_space.completion α), ennreal.of_real (uniform_space.completion.extension₂ has_dist.dist x y), edist_dist := _, to_uniform_space := uniform_space.completion.uniform_space α metric_space.to_uniform_space', uniformity_dist := _}
The embedding of a metric space in its completion is an isometry.