perfectSpace_iff_forall_not_isolated

English

A space is perfect if and only if every point is not isolated in the punctured neighborhood.

Русский

Пространство совершенное тогда и только тогда, когда у каждой точки нет изолированной окрестности в удалении точки.

LaTeX

$$$\text{PerfectSpace } X \iff \forall x:\,X, \mathcal{N}_{x}^{\neq} \text{ NeBot}.$$$

Lean4

theorem perfectSpace_iff_forall_not_isolated : PerfectSpace X ↔ ∀ x : X, Filter.NeBot (𝓝[≠] x) := by
  simp [perfectSpace_def, Preperfect, AccPt]

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