English
In a nontrivial separable densely ordered α, there exists a countable dense set s ⊆ α that contains neither bottom nor top elements of α.
Русский
В ненулевом разделимом плотном упорядоченном пространстве α существует счетное плотное множество s ⊆ α, не содержащее ни минимального, ни максимального элемента.
LaTeX
$$$\\exists s\\subseteq α\\; (s\\text{ countable})\\land Dense\\ s\\land (\\forall x, IsBot(x) \\rightarrow x \\notin s) \\land (\\forall x, IsTop(x) \\rightarrow x \\notin s).$$$
Lean4
/-- If `α` is a nontrivial separable dense linear order, then there exists a
countable dense set `s : Set α` that contains neither top nor bottom elements of `α`.
For a dense set containing both bot and top elements, see
`exists_countable_dense_bot_top`. -/
theorem exists_countable_dense_no_bot_top [SeparableSpace α] [Nontrivial α] :
∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s := by
simpa using dense_univ.exists_countable_dense_subset_no_bot_top
