English
Let ε ≥ 0 and δ ≥ 0. For any set s, thickening ε (cthickening δ s) = thickening (ε+δ) s.
Русский
Пусть ε ≥ 0 и δ ≥ 0. Для любого множества s верно: thickening ε (cthickening δ s) = thickening (ε+δ) s.
LaTeX
$$$$\forall s\subseteq E:\; \operatorname{thickening}(\varepsilon, \operatorname{cthickening}(\delta, s)) = \operatorname{thickening}(\varepsilon+\delta, s), \quad \varepsilon \ge 0,\ \delta \ge 0.$$$$
Lean4
@[simp]
theorem cthickening_thickening (hε : 0 ≤ ε) (hδ : 0 < δ) (s : Set E) :
cthickening ε (thickening δ s) = cthickening (ε + δ) s :=
(cthickening_thickening_subset hε _ _).antisymm fun x =>
by
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEdist_thickening hδ]
exact
tsub_le_iff_right.2
-- Note: `interior (cthickening δ s) ≠ thickening δ s` in general
