cthickening_eq_iInter_thickening — Mathlib

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ε

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