Theorems · Theorem · general topology

Dense.exists_countable_dense_subset_bot_top

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s],
  Dense s → ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

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.

Defined in

Mathlib.Topology.Bases

Cited by

3 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpacePartialOrderTopologicalSpace.SeparableSpace