hausdorffDist_closure₁ — Mathlib

English

Replacing a set by its closure does not change the Hausdorff distance: hausdorffDist(closure(s), t) = hausdorffDist(s, t).

Русский

Замена множества его замыканием не меняет расстояние Хаусдорфа: hausdorffDist(closure(s), t) = hausdorffDist(s, t).

LaTeX

$$$\operatorname{hausdorffDist}(\overline{s},t)=\operatorname{hausdorffDist}(s,t).$$$

Lean4

/-- Replacing a set by its closure does not change the Hausdorff distance. -/
@[simp]
theorem hausdorffDist_closure₁ : hausdorffDist (closure s) t = hausdorffDist s t := by simp [hausdorffDist]

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