denseRange_denseSeq — Mathlib

English

The canonical dense sequence denseSeq α has dense range.

Русский

Устойчивая плотная последовательность denseSeq α имеет плотный диапазон.

LaTeX

$$$\\text{DenseRange}(\\text{denseSeq }\\alpha)$$$

Lean4

/-- The sequence `TopologicalSpace.denseSeq α` has dense range. -/
@[simp]
theorem denseRange_denseSeq [SeparableSpace α] [Nonempty α] : DenseRange (denseSeq α) :=
  Classical.choose_spec (exists_dense_seq α)

Похожие утверждения