English
If hε ≥ 0, then cthickening ε(thickening δ s) ⊆ cthickening ε+δ s.
Русский
Если hε ≥ 0, то cthickening ε(thickening δ s) ⊆ cthickening(ε+δ) s.
LaTeX
$$$\operatorname{cthickening}_{\varepsilon}(\operatorname{thickening}_{\delta}(s)) \subseteq \operatorname{cthickening}_{\varepsilon+\delta}(s)$$$
Lean4
/-- For the equality, see `thickening_cthickening`. -/
@[simp]
theorem thickening_cthickening_subset (ε : ℝ) (hδ : 0 ≤ δ) (s : Set α) :
thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s :=
by
obtain hε | hε := le_total ε 0
· simp only [thickening_of_nonpos hε, empty_subset]
intro x
simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEdist_lt_iff, ENNReal.ofReal_add hε hδ]
rintro ⟨y, hy, hxy⟩
exact
infEdist_le_edist_add_infEdist.trans_lt
(ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)
