α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b})
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable {x | 𝓝[Ioi x] x = ⊥}
simp only [nhdsWithin_Ioi_eq_bot_iff, setOf_or]
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b})
exact (subsingleton_isTop α).countable.union countable_setOf_covby_right