cthickening_eq_iInter_cthickening

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ε

Похожие утверждения