countable_of_Lindelof_of_discrete

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#countable_of_Lindelof_of_discrete

← MathLib Explorer

English

A Lindelöf space X that is discrete is countable.

Русский

Линдельфово пространство X, которое дискретно, счётно.

LaTeX

$$$[LindelofSpace X]\,[DiscreteTopology X]\Rightarrow Countable X$$$

Lean4

theorem countable_of_Lindelof_of_discrete [LindelofSpace X] [DiscreteTopology X] : Countable X :=
  countable_univ_iff.mp isLindelof_univ.countable_of_discrete

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

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

Разделы

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

Аффилиация

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