neBot_nhdsWithin_compl_of_nontrivial_of_t1space

English

In a nontrivial connected T1 space, every point is a limit point of the space minus itself.

Русский

В ненулевом связном T1-пространстве каждая точка является точкой предела пространства за вычетом самой точки.

LaTeX

$$$\text{ConnectedSpace}(X) \land \text{Nontrivial}(X) \land \text{T1Space}(X) \Rightarrow \forall x\in X,\ x \text{ is a limit point of } X\setminus\{x\}$$$

Lean4

/-- A non-trivial connected T1 space has no isolated points. -/
instance (priority := 100) neBot_nhdsWithin_compl_of_nontrivial_of_t1space [ConnectedSpace X] [Nontrivial X] [T1Space X]
    (x : X) : NeBot (𝓝[≠] x) := by
  by_contra contra
  rw [not_neBot, ← isOpen_singleton_iff_punctured_nhds] at contra
  replace contra :=
    nonempty_inter isOpen_compl_singleton contra (compl_union_self _) (Set.nonempty_compl_of_nontrivial _)
      (singleton_nonempty _)
  simp [compl_inter_self { x }] at contra

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