nhdsNE_sup_pure — Mathlib

English

The union (supremum) of the punctured neighborhood and the pure neighborhood equals the neighborhood.

Русский

Объединение (супремум) пунктированной окрестности и чистой окрестности равняется окрестности.

LaTeX

$$$$ 𝓝_{\\neq} a \\; \\sqcup \\; \\mathrm{pure}(a) = 𝓝(a) $$$$

Lean4

@[simp]
theorem nhdsNE_sup_pure (a : α) : 𝓝[≠] a ⊔ pure a = 𝓝 a := by
  rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]

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