metric.has_dist

The distance on the completion is obtained by extending the distance on the original space, by uniform continuity.

metric.completion.uniform_continuous_dist

The new distance is uniformly continuous.

metric.completion.dist_eq

The new distance is an extension of the original distance.

metric.completion.mem_uniformity_dist

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

metric.completion.eq_of_dist_eq_zero

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

metric.completion.metric_space

Metric space structure on the completion of a metric space.

metric.completion.coe_isometry

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