English
The Hausdorff distance is invariant under the image of an isometry: hausdorffDist (Set.image Φ s) (Set.image Φ t) = hausdorffDist s t.
Русский
Расстояние Хаусдорфа сохраняется после изображения через изометрию: hausdorffDist(Set.image Φ s)(Set.image Φ t) = hausdorffDist s t.
LaTeX
$$$\operatorname{hausdorffDist}(\operatorname{Set.image}(\Phi,s), \operatorname{Set.image}(\Phi,t)) = \operatorname{hausdorffDist}(s,t).$$$
Lean4
/-- The Hausdorff distance is invariant under isometries. -/
theorem hausdorffDist_image (h : Isometry Φ) : hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t := by
simp [hausdorffDist, hausdorffEdist_image h]