isometry_iff_dist_eq — Mathlib

English

On pseudometric spaces, an isometry preserves distances exactly.

Русский

На псевдометрике изометрия сохраняет расстояния точно.

LaTeX

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

Lean4

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

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