English
Let δ ≥ 0. Then the δ-thickening of E equals the intersection of the ε-thickenings of E over all ε with ε > δ.
Русский
Пусть δ ≥ 0. Тогда δ-уплотнение E равно пересечению ε-уплотнений E по всем ε > δ.
LaTeX
$$$\operatorname{cthickening}_{\delta} E = \bigcap_{\varepsilon>\delta} \operatorname{thickening}_{\varepsilon} E$$$
Lean4
theorem cthickening_eq_iInter_thickening {δ : ℝ} (δ_nn : 0 ≤ δ) (E : Set α) :
cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), thickening ε E :=
by
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
exact fun _ hε => nonempty_Ioc.mpr hε