cthickening_eq_iInter_thickening''

English

For any δ, the δ-thickening of E equals the intersection over all ε > max(0, δ) of thickening ε E.

Русский

Для данного δ; E: ∀ε > max(0,δ) выполняется: δ-уплотнение E = ⋂_{ε>max(0,δ)} thickening_ε E.

LaTeX

$$$\operatorname{cthickening}_{\delta} E = \bigcap_{\varepsilon>\max\{0,\delta\}} \operatorname{thickening}_{\varepsilon} E$$$

Lean4

theorem cthickening_eq_iInter_thickening'' (δ : ℝ) (E : Set α) :
    cthickening δ E = ⋂ (ε : ℝ) (_ : max 0 δ < ε), thickening ε E :=
  by
  rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]
  exact le_max_left _ _

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