thickening_compl_thickening_self_subset_compl

English

The δ-thickening of the complement of the δ-thickening of a set is contained in the complement of the set.

Русский

δ-уплотнение дополнения δ-уплотнения множества содержится в дополнении самого множества.

LaTeX

$$$thickening\\,δ\\,(thickening\\,δ\\,E)^{c} \\subseteq E^{c}$$$

Lean4

/-- The δ-thickening of the complement of the δ-thickening of a set is contained in the complement
of the set. -/
theorem thickening_compl_thickening_self_subset_compl (δ : ℝ) (E : Set α) : thickening δ (thickening δ E)ᶜ ⊆ Eᶜ :=
  by
  apply compl_subset_compl.mp
  simpa only [compl_compl] using subset_compl_thickening_compl_thickening_self δ E

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