English
For any ε, δ real numbers, and any set s, the ε-thickening of the δ-thickening of s is contained in the (ε+δ)-thickening of s.
Русский
Для любых ε, δ действительных и множества 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 `thickening_thickening`. -/
@[simp]
theorem thickening_thickening_subset (ε δ : ℝ) (s : Set α) : thickening ε (thickening δ s) ⊆ thickening (ε + δ) s :=
by
obtain hε | hε := le_total ε 0
· simp only [thickening_of_nonpos hε, empty_subset]
obtain hδ | hδ := le_total δ 0
· simp only [thickening_of_nonpos hδ, thickening_empty, empty_subset]
intro x
simp_rw [mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add hε hδ]
exact fun ⟨y, ⟨z, hz, hy⟩, hx⟩ => ⟨z, hz, (edist_triangle _ _ _).trans_lt <| ENNReal.add_lt_add hx hy⟩
