instLindelofSpaceOfSigmaCompactSpace

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

A σ-compact space is Lindelöf.

Русский

σ-компактное пространство является Линдельфовым.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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