cthickening_cthickening_subset — Mathlib

English

The δ-thickening of the ε-thickening of a set is contained in the (δ+ε)-thickening of that set.

Русский

δ-уплотнение ε-уплотнения множества вложено в (δ+ε)-уплотнение этого множества.

LaTeX

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

Lean4

/-- For the equality, see `cthickening_cthickening`. -/
@[simp]
theorem cthickening_cthickening_subset (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set α) :
    cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s :=
  by
  intro x
  simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
  exact fun hx => infEdist_le_infEdist_cthickening_add.trans (add_le_add_right hx _)

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