English
Let f be an isometry class element between pseudo‑emetric spaces α and β. Then for all x,y ∈ α, the extended distance is preserved: edist(f(x), f(y)) = edist(x, y).
Русский
Пусть f является изометрией между псевдометрическими пространствами α и β. Тогда для любых x,y ∈ α сохраняется расширенное расстояние: edist(f(x), f(y)) = edist(x, y).
LaTeX
$$$ edist\,(f(x), f(y)) = edist\,(x, y). $$$
Lean4
protected theorem edist_eq (x y : α) : edist (f x) (f y) = edist x y :=
(IsometryClass.isometry f).edist_eq x y