English
In a pseudo-EMetric space, for any real δ and any set E, the δ-thickening of E equals the intersection of the ε-thickenings of E over all ε with ε > δ.
Русский
В псевдо-эмэтриковом пространстве для множества E и числа δ верно: δ-уплотнение E равно пересечению ε-уплотнений E для всех ε > δ.
LaTeX
$$$\operatorname{cthickening}_{\delta} E = \bigcap_{\varepsilon\in\mathbb{R},\ \delta<\varepsilon} \operatorname{cthickening}_{\varepsilon} E$$$
Lean4
theorem cthickening_eq_iInter_cthickening {δ : ℝ} (E : Set α) :
cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), cthickening ε E :=
by
apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
exact fun _ hε => nonempty_Ioc.mpr hε