English
Let s be a dense subset of α with partial order. If α is separable, then there exists a countable dense subset t ⊆ s such that t 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
/-- Let `s` be a dense set in a topological space `α` with partial order structure. 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` contains bottom/top element of `α` when they exist and belong
to `s`. For a dense subset containing neither bot nor top elements, see
`Dense.exists_countable_dense_subset_no_bot_top`. -/
theorem exists_countable_dense_subset_bot_top {α : Type*} [TopologicalSpace α] [PartialOrder α] {s : Set α}
[SeparableSpace s] (hs : Dense s) :
∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∈ s → x ∈ t) ∧ ∀ x, IsTop x → x ∈ s → x ∈ t :=
by
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
refine ⟨(t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
exacts [inter_subset_right, (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,
htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩, fun x hx hxs =>
⟨Or.inr <| Or.inr hx, hxs⟩]
