not_LindelofSpace_iff

Mathlib.Topology.Compactness.Lindelof

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

English

¬LindelofSpace X is equivalent to NonLindelofSpace X.

Русский

Не-Линдельфовость пространства эквивалентна NonLindelofSpace X.

LaTeX

$$$¬LindelofSpace X \iff NonLindelofSpace X$$$

Lean4

theorem not_LindelofSpace_iff : ¬LindelofSpace X ↔ NonLindelofSpace X :=
  ⟨fun h₁ => ⟨fun h₂ => h₁ ⟨h₂⟩⟩, fun ⟨h₁⟩ ⟨h₂⟩ => h₁ h₂⟩

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

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

Разделы

Аффилиация

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