isometry_iff_nndist_eq — Mathlib

English

On pseudometric spaces, being an isometry is equivalent to preserving all nonnegative distances.

Русский

На псевдометрике изометрия эквивалентна сохранению всех неотрицательных расстояний.

LaTeX

$$$Isometry\\ f \\iff \\forall x,y,\\ nndist(f(x),f(y)) = nndist(x,y).$$$

Lean4

/-- On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative
distances. -/
theorem isometry_iff_nndist_eq [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
    Isometry f ↔ ∀ x y, nndist (f x) (f y) = nndist x y := by simp only [Isometry, edist_nndist, ENNReal.coe_inj]

Похожие утверждения