pure_sup_nhdsNE — Mathlib

English

The supremum of the pure neighborhood at a and the punctured neighborhood equals the neighborhood at a.

Русский

Наибольшее объединение чистой окрестности в a и пунктированной окрестности равны окрестности в a.

LaTeX

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

Lean4

@[simp]
theorem pure_sup_nhdsNE (a : α) : pure a ⊔ 𝓝[≠] a = 𝓝 a := by rw [← sup_comm, nhdsNE_sup_pure]

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