closure_eq_iInter_cthickening — Mathlib

English

The closure of E equals the intersection over δ>0 of cthickening δ E.

Русский

Замыкание E равняется пересечению δ>0 cthickening δ E.

LaTeX

$$$\operatorname{closure} E = \bigcap_{δ>0} \operatorname{cthickening}_{δ} E$$$

Lean4

/-- The closure of a set equals the intersection of its closed thickenings of positive radii. -/
theorem closure_eq_iInter_cthickening (E : Set α) : closure E = ⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ E :=
  by
  rw [← cthickening_zero]
  exact cthickening_eq_iInter_cthickening E

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