thickening_mem_nhdsSet — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem thickening_mem_nhdsSet (E : Set α) {δ : ℝ} (hδ : 0 < δ) : thickening δ E ∈ 𝓝ˢ E :=
  isOpen_thickening.mem_nhdsSet.2 <| self_subset_thickening hδ E

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