exists_nhds_ne_neBot — Mathlib

English

In a compact infinite space, there exists a point z whose punctured neighborhood is nontrivial.

Русский

В компактном бесконечном пространстве существует точка z, для которой punctured окрестности не тривиальна.

LaTeX

$$$\\exists z \\in X, (\\\\mathcal{N}_{X \\setminus \\{z\\}}(z)).\\\\NeBot$$$

Lean4

theorem exists_nhds_ne_neBot (X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] : ∃ z : X, (𝓝[≠] z).NeBot :=
  by simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal

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