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 _)