English
If s is dense in a nontrivial densely ordered α and s is a separable space, then there exists a countable dense subset t ⊆ s that avoids bottom/top elements of α.
Русский
Если s плотно в ненулевом плотном линейно упорядоченном пространстве α и пространство s разделимо, то существует счетное плотное подмножество t ⊆ s, не содержащее нижних и верхних точек α.
LaTeX
$$$\\exists t\\subseteq s\\; (t\\text{ countable})\\land (Dense\\ t) \\land (\\forall x, IsBot(x) \\rightarrow x \\notin t) \\land (\\forall x, IsTop(x) \\rightarrow x \\notin t).$$$
Lean4
/-- Let `s` be a dense set in a nontrivial dense linear order `α`. If `s` is a
separable space (e.g., if `α` has a second countable topology), then there exists a countable
dense subset `t ⊆ s` such that `t` does not contain bottom/top elements of `α`. -/
theorem exists_countable_dense_subset_no_bot_top [Nontrivial α] {s : Set α} [SeparableSpace s] (hs : Dense s) :
∃ t, t ⊆ s ∧ t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∉ t) ∧ ∀ x, IsTop x → x ∉ t :=
by
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
refine ⟨t \ ({x | IsBot x} ∪ {x | IsTop x}), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
· exact diff_subset.trans hts
· exact htc.mono diff_subset
· exact htd.diff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)
· simp [hx]
· simp [hx]
