English
Replacing s by its closure does not change the Hausdorff distance with t, i.e., d_H(closure s, t) = d_H(s, t).
Русский
Замена s на его замыкание не меняет расстояния Хаусдорфа до t: d_H(closure s, t) = d_H(s, t).
LaTeX
$$$ \operatorname{hausdorffEdist}(\overline{s}, t) = \operatorname{hausdorffEdist}(s,t) $$$
Lean4
/-- Replacing a set by its closure does not change the Hausdorff edistance. -/
@[simp]
theorem hausdorffEdist_closure₁ : hausdorffEdist (closure s) t = hausdorffEdist s t :=
by
refine le_antisymm ?_ ?_
·
calc
_ ≤ hausdorffEdist (closure s) s + hausdorffEdist s t := hausdorffEdist_triangle
_ = hausdorffEdist s t := by simp [hausdorffEdist_comm]
·
calc
_ ≤ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t := hausdorffEdist_triangle
_ = hausdorffEdist (closure s) t := by simp
