hausdorffEdist_image — Mathlib

English

The Hausdorff edistance is preserved under images by an isometry: d_H(Φ[S], Φ[T]) = d_H(S,T).

Русский

Расстояние Хаусдорфа сохраняется при отображении изометрией: d_H(Φ[S], Φ[T]) = d_H(S,T).

LaTeX

$$$ \text{Isometry } \Phi \Rightarrow \operatorname{hausdorffEdist}(\Phi[S], \Phi[T]) = \operatorname{hausdorffEdist}(S,T) $$$

Lean4

/-- The Hausdorff edistance is invariant under isometries. -/
theorem hausdorffEdist_image (h : Isometry Φ) : hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t := by
  simp only [hausdorffEdist_def, iSup_image, infEdist_image h]

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