infDist_le_infDist_add_hausdorffDist

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

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