cthickening_thickening_subset — Mathlib

English

As a simplification, thickening ε(thickening δ s) ⊆ thickening (ε+δ) s.

Русский

Упрощенно: thickening_ε(thickening_δ(s)) ⊆ thickening_{ε+δ}(s).

LaTeX

$$$\operatorname{thickening}_{\varepsilon}(\operatorname{thickening}_{\delta}(s)) \subseteq \operatorname{thickening}_{\varepsilon+\delta}(s)$$$

Lean4

/-- For the equality, see `cthickening_thickening`. -/
@[simp]
theorem cthickening_thickening_subset (hε : 0 ≤ ε) (δ : ℝ) (s : Set α) :
    cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s :=
  by
  obtain hδ | hδ := le_total δ 0
  · simp only [thickening_of_nonpos hδ, cthickening_empty, empty_subset]
  intro x
  simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
  exact fun hx => infEdist_le_infEdist_thickening_add.trans (add_le_add_right hx _)

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