closure_subset_thickening — Mathlib

English

The closure of E is contained in thickening δ E whenever δ > 0.

Русский

Замыкание E содержится в thickening δ E при δ > 0.

LaTeX

$$closure E ⊆ thickening δ E for δ > 0$$

Lean4

/-- The (open) thickening of a set contains the closure of the set. -/
theorem closure_subset_thickening {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : closure E ⊆ thickening δ E :=
  by
  rw [← cthickening_zero]
  exact cthickening_subset_thickening' δ_pos δ_pos E

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