English
The closure of E equals the intersection over a directed family of closed thickenings with radii δ accumulating at zero, provided the radii are positive and dense near zero. More precisely, for E, s with appropriate accumulation, closure E = ⋂ δ∈s cthickening δ E.
Русский
Замыкание E есть пересечение cthickening δ E по δ из множества s, если δ > 0 и s бесконечно стремится к нулю сверху.
LaTeX
$$$\operatorname{closure} E = \bigcap_{\delta\in s} \operatorname{cthickening}_{\delta} E$$$
Lean4
/-- The closure of a set equals the intersection of its closed thickenings of positive radii
accumulating at zero. -/
theorem closure_eq_iInter_cthickening' (E : Set α) (s : Set ℝ) (hs : ∀ ε, 0 < ε → (s ∩ Ioc 0 ε).Nonempty) :
closure E = ⋂ δ ∈ s, cthickening δ E := by
by_cases hs₀ : s ⊆ Ioi 0
· rw [← cthickening_zero]
apply cthickening_eq_iInter_cthickening' _ hs₀ hs
obtain ⟨δ, hδs, δ_nonpos⟩ := not_subset.mp hs₀
rw [Set.mem_Ioi, not_lt] at δ_nonpos
apply Subset.antisymm
· exact subset_iInter₂ fun ε _ => closure_subset_cthickening ε E
· rw [← cthickening_of_nonpos δ_nonpos E]
exact biInter_subset_of_mem hδs
