nhdsNE_le_cofinite — Mathlib

English

In any T1 space α, for every a, the punctured neighborhoods satisfy 𝓝[≠] a ≤ coffinite.

Русский

В любом T1-пространстве α окрестности без точки удовлетворяют 𝓝[≠] a ≤ cofinitive.

LaTeX

$$$ \\forall a,\\ 𝓝[≠] a \\leq \\operatorname{cofinite}. $$$

Lean4

theorem nhdsNE_le_cofinite {α : Type*} [TopologicalSpace α] [T1Space α] (a : α) : 𝓝[≠] a ≤ cofinite :=
  by
  refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_
  rcases eq_or_ne a x with rfl | hx
  exacts [self_mem_nhdsWithin, eventually_ne_nhdsWithin hx]

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