coLindelof_neBot_iff

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#Filter.coLindelof_neBot_iff

English

There is an equivalence: NeBot (Filter.coLindelof X) iff NonLindelofSpace X.

Русский

Существует эквивалентность: NeBot(coLindelof X) ⇔ NonLindelofSpace X.

LaTeX

$$$[NeBot (Filter.coLindelof X)] \iff NonLindelofSpace X$$$

Lean4

theorem coLindelof_neBot_iff : NeBot (Filter.coLindelof X) ↔ NonLindelofSpace X :=
  ⟨nonLindelofSpace_of_neBot, fun _ => inferInstance⟩

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

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

Разделы

Аффилиация

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