English
In a T1 space, punctured neighborhoods remain punctured neighborhoods after removing a finite set of points.
Русский
В T1-пространстве punctured окрестности остаются punctured после удаления конечного множества точек.
LaTeX
$$$\text{nhdsNE}_x \text{ within } (U) \; \&\; \text{Finite}(s) \Rightarrow U \setminus s \in \text{nhdsNE}_x.$$$
Lean4
/-- In a T1Space, punctured neighborhoods are stable under removing finite sets of points. -/
theorem nhdsNE_of_nhdsNE_sdiff_finite {X : Type*} [TopologicalSpace X] [T1Space X] {x : X} {U s : Set X}
(hU : U ∈ 𝓝[≠] x) (hs : Finite s) : U \ s ∈ 𝓝[≠] x :=
by
rw [mem_nhdsWithin] at hU ⊢
obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU
use t \ (s \ { x })
constructor
· rw [← isClosed_compl_iff, compl_diff]
exact s.toFinite.diff.isClosed.union (isClosed_compl_iff.2 ht)
· tauto_set
