LindelofSpace

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#Quotient.LindelofSpace

English

The quotient of a Lindelöf space remains Lindelöf.

Русский

Факторпространство Линдельфово

LaTeX

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

Lean4

instance LindelofSpace {s : Setoid X} [LindelofSpace X] : LindelofSpace (Quotient s) :=
  Quot.LindelofSpace

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

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

Разделы

Аффилиация

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