isLindelof_univ_iff

Mathlib.Topology.Compactness.Lindelof

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

English

IsLindelof(univ) iff LindelöfSpace X.

Русский

IsLindelöf(универсум) эквивалентно LindelofSpace X.

LaTeX

$$$IsLindelof(\mathrm{univ}) \iff \mathrm{LindelofSpace}(X)$$$

Lean4

theorem isLindelof_univ_iff : IsLindelof (univ : Set X) ↔ LindelofSpace X :=
  ⟨fun h => ⟨h⟩, fun h => h.1⟩

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

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

Разделы

Аффилиация

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