English
Under suitable conditions, cthickening δ E equals the intersection over ε of cthickening ε E.
Русский
При определённых условиях cthickening δ E равняется пересечению по ε от cthickening ε E.
LaTeX
$$$\\mathrm{cthickening}_{\\delta}(E) = \\bigcap_{\\varepsilon} \\mathrm{cthickening}_{\\varepsilon}(E) \\quad(\\text{при некоторых условиях}).$$$
Lean4
theorem cthickening_eq_iInter_cthickening' {δ : ℝ} (s : Set ℝ) (hsδ : s ⊆ Ioi δ)
(hs : ∀ ε, δ < ε → (s ∩ Ioc δ ε).Nonempty) (E : Set α) : cthickening δ E = ⋂ ε ∈ s, cthickening ε E :=
by
apply Subset.antisymm
· exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E
· unfold cthickening
intro x hx
simp only [mem_iInter, mem_setOf_eq] at *
apply ENNReal.le_of_forall_pos_le_add
intro η η_pos _
rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩
apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans
rw [ENNReal.coe_nnreal_eq η]
exact ENNReal.ofReal_add_le
