English
In a second-countable space, the set of points for which the right neighborhood 𝓝[>] x is the bottom element is countable.
Русский
Во втором счётном пространстве множество точек, для которых правая окрестность равна нижнему элементу, счётно.
LaTeX
$$$[\text{SecondCountableTopology}(\alpha)] \Rightarrow \{x : \alpha \mid \mathcal{N}_{[>]} x = \bot\}.\text{Countable}$$$
Lean4
theorem nhdsGT_eq_bot_iff {a : α} : 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b :=
by
by_cases ha : IsTop a
· simp [ha, ha.isMax.Ioi_eq]
· simp only [ha, false_or]
rw [isTop_iff_isMax, not_isMax_iff] at ha
simp only [(nhdsGT_basis_of_exists_gt ha).eq_bot_iff, covBy_iff_Ioo_eq]