English
Let α be a separable space with partial order. If s is a dense subset of α, then there exists a countable dense t ⊆ s that contains all bottom elements and all top elements of α that lie in s.
Русский
Пусть α — сепарабельное пространство с частичным порядком. Если s плотное подмножество α, то найдется счетное плотное t ⊆ s, содержащее все нижние и верхние элементы α, принадлежащие s.
LaTeX
$$$\exists t \subseteq s,\ t.Countable ∧ Dense(t) ∧ (∀ x, IsBot(x) \to x \in s \to x \in t) ∧ (∀ x, IsTop(x) \to x \in s \to x \in t)$$$
Lean4
/-- If `α` is a separable topological space with a partial order, then there exists a countable
dense set `s : Set α` that contains those of both bottom and top elements of `α` that actually
exist. For a dense set containing neither bot nor top elements, see
`exists_countable_dense_no_bot_top`. -/
theorem exists_countable_dense_bot_top (α : Type*) [TopologicalSpace α] [SeparableSpace α] [PartialOrder α] :
∃ 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_bot_top
