cthickening_mem_nhdsSet — Mathlib

English

For E ⊆ α and δ > 0, a closed thickening δ E is a neighborhood of E: cthickening δ E ∈ 𝓝ˢ E.

Русский

Пусть E ⊆ α и δ > 0. Тогда закрытое утолщение δ E является окрестностью E: cthickening δ E ∈ 𝓝ˢ E.

LaTeX

$$$\\text{cthickening}_{\\delta}(E) \\in \\mathcal{N}^{\\mathrm{s}}(E) \\quad(\\delta > 0).$$$

Lean4

theorem cthickening_mem_nhdsSet (E : Set α) {δ : ℝ} (hδ : 0 < δ) : cthickening δ E ∈ 𝓝ˢ E :=
  mem_of_superset (thickening_mem_nhdsSet E hδ) (thickening_subset_cthickening _ _)

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