denseSeq

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.denseSeq

Lean4

/-- A dense sequence in a non-empty separable topological space.

If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`. -/
def denseSeq [SeparableSpace α] [Nonempty α] : ℕ → α :=
  Classical.choose (exists_dense_seq α)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru