closure_subset_cthickening — Mathlib

English

The closure of E is contained in cthickening δ E for any δ.

Русский

Замыкание E включено в cthickening δ E для любых δ.

LaTeX

$$closure E ⊆ cthickening δ E$$

Lean4

/-- The closed thickening of a set contains the closure of the set. -/
theorem closure_subset_cthickening (δ : ℝ) (E : Set α) : closure E ⊆ cthickening δ E :=
  by
  rw [← cthickening_of_nonpos (min_le_right δ 0)]
  exact cthickening_mono (min_le_left δ 0) E

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