English
If f: α → β is an isometry between metric spaces, its extension to the completion of α is an isometry into β.
Русский
Если отображение f: α → β есть изометрия, то его продолжение до завершения α также является изометрией.
LaTeX
$$$\text{Isometry}(f) \Rightarrow \text{Isometry}(\mathrm{Completion}.extension f).$$$
Lean4
/-- One gets a metric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the metric space and the emetric space. In this definition, the distance
is given separately, to be able to prescribe some expression which is not defeq to the push-forward
of the edistance to reals. -/
abbrev toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ) (edist_ne_top : ∀ x y : α, edist x y ≠ ⊤)
(h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) : MetricSpace α :=
@MetricSpace.ofT0PseudoMetricSpace _ (PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist edist_ne_top h) _
