no goals
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
a b : α
s : Set α
l : Filter β
f : α → β
inst✝¹ : SeparableSpace α
inst✝ : Nontrivial α
⊢ ∃ s, Set.Countable s ∧ Dense s ∧ (∀ (x : α), IsBot x → ¬x ∈ s) ∧ ∀ (x : α), IsTop x → ¬x ∈ s
simpa using dense_univ.exists_countable_dense_subset_no_bot_top