nhdsGT_eq_bot_iff — Mathlib

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]

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