closure_eq_iInter_thickening' — Mathlib

English

If s is a set of radii dense near zero and δ>0, the closure of E equals the intersection of thickening δ E over δ in s, with the accumulation condition.

Русский

Если набор радиусов близок к нулю и δ>0, замыкание E равно пересечению thickening δ E по δ в s.

LaTeX

$$$\operatorname{closure} E = \bigcap_{δ\in s} \operatorname{thickening}_{δ} E$$$

Lean4

/-- The closure of a set equals the intersection of its open thickenings of positive radii
accumulating at zero. -/
theorem closure_eq_iInter_thickening' (E : Set α) (s : Set ℝ) (hs₀ : s ⊆ Ioi 0)
    (hs : ∀ ε, 0 < ε → (s ∩ Ioc 0 ε).Nonempty) : closure E = ⋂ δ ∈ s, thickening δ E :=
  by
  rw [← cthickening_zero]
  apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs

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