English
A nonempty separable space α admits a dense sequence u: ℕ → α with dense range.
Русский
Непустое разделимое пространство α допускает плотную последовательность u: ℕ → α с плотным образом
LaTeX
$$$\\exists u:\\mathbb{N}\\to \\alpha,\\ DenseRange(u)$$$
Lean4
/-- A nonempty separable space admits a sequence with dense range. Instead of running `cases` on the
conclusion of this lemma, you might want to use `TopologicalSpace.denseSeq` and
`TopologicalSpace.denseRange_denseSeq`.
If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`. -/
theorem exists_dense_seq [SeparableSpace α] [Nonempty α] : ∃ u : ℕ → α, DenseRange u :=
by
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs
exact ⟨u, s_dense.mono hu⟩
