exists_countable_dense

Mathlib.Topology.Bases

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

English

In any separable space α, there exists a countable dense subset.

Русский

В любом разделимом пространстве α существует счётное плотное подмножество.

LaTeX

$$$\\exists s\\subseteq \\alpha,\\ s.\\text{Countable} \\wedge \\overline{s}=\\alpha$$$

Lean4

theorem exists_countable_dense [SeparableSpace α] : ∃ s : Set α, s.Countable ∧ Dense s :=
  SeparableSpace.exists_countable_dense

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

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

Разделы

Аффилиация

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