to_Lindelof

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#HereditarilyLindelof.to_Lindelof

← MathLib Explorer

English

If X is hereditarily Lindelöf, then X is Lindelöf.

Русский

Если X наследовательно Линдельфово, то X Линдельфово.

LaTeX

$$$[HereditarilyLindelofSpace X] \\Rightarrow \\operatorname{LindelofSpace}(X).$$$

Lean4

instance (priority := 100) to_Lindelof [HereditarilyLindelofSpace X] : LindelofSpace X where
  isLindelof_univ := HereditarilyLindelofSpace.isHereditarilyLindelof_univ.isLindelof

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

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

Разделы

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

Аффилиация

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