self_subset_cthickening — Mathlib

English

For any set E and any real δ, a set is contained in its closed δ-thickening: E ⊆ cthickening δ E.

Русский

Для любой множества E и любого действительного числа δ верно: E ⊆ cthickening δ E.

LaTeX

$$$E \\subseteq \\mathrm{cthickening}_{\\delta}(E)$$$

Lean4

/-- A set is contained in its own closed thickening. -/
theorem self_subset_cthickening {δ : ℝ} (E : Set α) : E ⊆ cthickening δ E :=
  subset_closure.trans (closure_subset_cthickening δ E)

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