English
If the punctured neighborhoods form a nontrivial filter, then every neighborhood of x is infinite.
Русский
Если непустые окрестности с дыркой образуют непустой фильтр, то любая окрестность x бесконечна.
LaTeX
$$$\text{NeBot}(\mathcal{N}[\neq](x)) \Rightarrow \forall s \in \mathcal{N}(x), \; s \text{ is infinite}$$$
Lean4
/-- If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is
infinite. -/
theorem infinite_of_mem_nhds {X} [TopologicalSpace X] [T1Space X] (x : X) [hx : NeBot (𝓝[≠] x)] {s : Set X}
(hs : s ∈ 𝓝 x) : Set.Infinite s := by
refine fun hsf => hx.1 ?_
rw [← isOpen_singleton_iff_punctured_nhds]
exact isOpen_singleton_of_finite_mem_nhds x hs hsf
