English
Let δ ≥ 0. Let S be a set of radii with S ⊆ (δ, ∞) and such that for every ε > δ there exists ε′ ∈ S with δ < ε′ ≤ ε and (S ∩ (δ, ε]) is nonempty. Then for every E, cthickening δ E equals the intersection over ε ∈ S of thickening ε E.
Русский
Пусть δ ≥ 0. Пусть S ⊆ (δ, ∞) и для каждого ε > δ существует ε′ ∈ S с δ < ε′ ≤ ε и (S ∩ (δ, ε]) непусто. Тогда для любого E выполнено: cthickening δ E = ⋂_{ε∈S} thickening ε E.
LaTeX
$$$\text{cthickening}_{\delta} E = \bigcap_{\varepsilon\in S} \text{thickening}_{\varepsilon} E \quad(δ\ge 0,\ S\subseteq(δ,\infty),\ \forall ε>δ\, (S\cap(δ,ε]).\Nonempty)$$$$
Lean4
theorem cthickening_eq_iInter_thickening' {δ : ℝ} (δ_nn : 0 ≤ δ) (s : Set ℝ) (hsδ : s ⊆ Ioi δ)
(hs : ∀ ε, δ < ε → (s ∩ Ioc δ ε).Nonempty) (E : Set α) : cthickening δ E = ⋂ ε ∈ s, thickening ε E :=
by
refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_
· obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
exact ss.trans (thickening_mono hε'.2 E)
· rw [cthickening_eq_iInter_cthickening' s hsδ hs E]
exact iInter₂_mono fun ε _ => thickening_subset_cthickening ε E
