no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable {x | ∃ y, y < x ∧ Ioo y x = ∅}
simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_left