hausdorffDist_closure₂ — Mathlib

English

Let S and T be subsets of a metric space. Replacing T by its closure does not change the Hausdorff distance from S to T.

Русский

Пусть S и T — подмножества метрического пространства. Замена T на его замыкание не изменяет расстояние Хаусдорфа между S и T.

LaTeX

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

Lean4

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

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