instLindelofSpaceOfCompactSpace

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

Every compact space is Lindelöf.

Русский

Каждое компактное пространство Линдельфово.

LaTeX

$$$[{X]$ [TopologicalSpace X]}\,[{CompactSpace X}] \Rightarrow LindelofSpace X$$$

Lean4

/-- A compact space `X` is Lindelöf. -/
instance (priority := 100) [CompactSpace X] : LindelofSpace X :=
  { isLindelof_univ := isCompact_univ.isLindelof }

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

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

Разделы

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

Аффилиация

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