English
The Hausdorff distance is invariant under isometries: if Φ is an isometry, then hausdorffDist(Φ''s, Φ''t) = hausdorffDist(s, t).
Русский
Расстояние Хаусдорфа сохраняется под изометриями: если Φ—изометрия, то hausdorffDist(Φ''s, Φ''t) = hausdorffDist(s, t).
LaTeX
$$$\operatorname{hausdorffDist}(\Phi''s, \Phi''t) = \operatorname{hausdorffDist}(s,t).$$$
Lean4
/-- The infimum distance to `s` and `t` are the same, up to the Hausdorff distance
between `s` and `t` -/
theorem infDist_le_infDist_add_hausdorffDist (fin : hausdorffEdist s t ≠ ⊤) :
infDist x t ≤ infDist x s + hausdorffDist s t :=
by
refine toReal_le_add' infEdist_le_infEdist_add_hausdorffEdist (fun h ↦ ?_) (flip absurd fin)
rw [infEdist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢
rw [hausdorffEdist_comm] at fin
exact mt (nonempty_of_hausdorffEdist_ne_top · fin) h