countable_setOf_isolated_right — Mathlib

English

In a second-countable space, the set of points with 𝓝[>] x = ⊥ is countable.

Русский

Во втором счётном пространстве множество точек, у которых 𝓝[>] x = ⊥, счетно.

LaTeX

$$$[\text{SecondCountableTopology }\alpha] \Rightarrow \{x : \alpha \mid \mathcal{N}_{[>]} x = \bot\}.\text{Countable}$$$

Lean4

/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_right [SecondCountableTopology α] : {x : α | 𝓝[>] x = ⊥}.Countable :=
  by
  simp only [nhdsGT_eq_bot_iff, setOf_or]
  exact (subsingleton_isTop α).countable.union countable_setOf_covBy_right

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