hausdorffEdist_closure₂ — Mathlib

English

Replacing both sets by their closures leaves the Hausdorff distance unchanged: d_H(closure s, closure t) = d_H(s, t).

Русский

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

LaTeX

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

Lean4

/-- Replacing a set by its closure does not change the Hausdorff edistance. -/
@[simp]
theorem hausdorffEdist_closure₂ : hausdorffEdist s (closure t) = hausdorffEdist s t := by
  simp [@hausdorffEdist_comm _ _ s _]

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