to_separableSpace

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Countable.to_separableSpace

← MathLib Explorer

English

If α is countable, then α is a separable space.

Русский

Если пространство счётно, то оно разделимо.

LaTeX

$$$\\text{Countable}(\\alpha) \\Rightarrow \\text{SeparableSpace}(\\alpha)$$$

Lean4

instance (priority := 100) to_separableSpace [Countable α] : SeparableSpace α where
  exists_countable_dense := ⟨Set.univ, Set.countable_univ, dense_univ⟩

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

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

Разделы

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

Аффилиация

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