closure_eq_iInter_thickening — Mathlib

English

For any δ, the δ-thickening E equals the intersection over ε>δ of thickening ε E.

Русский

Для любого δ ∈ ℝ: δ-уплотнение E равно пересечению ε-уплотнений E для всех ε>δ.

LaTeX

$$$\operatorname{cthickening}_{\delta} E = \bigcap_{\varepsilon>\delta} \operatorname{thickening}_{\varepsilon} E$$$

Lean4

/-- The closure of a set equals the intersection of its (open) thickenings of positive radii. -/
theorem closure_eq_iInter_thickening (E : Set α) : closure E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E :=
  by
  rw [← cthickening_zero]
  exact cthickening_eq_iInter_thickening rfl.ge E

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