cocompact_neBot_iff

Mathlib.Topology.Compactness.Compact

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

English

The cocompact filter is nontrivial if and only if the space is noncompact.

Русский

Фильтр cocompact не тривиален тогда и только тогда, когда пространство не компактно.

LaTeX

$$NeBot (Filter.cocompact X) ↔ NoncompactSpace X$$

Lean4

theorem cocompact_neBot_iff : NeBot (Filter.cocompact X) ↔ NoncompactSpace X :=
  ⟨noncompactSpace_of_neBot, fun _ => inferInstance⟩

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

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

Разделы

Аффилиация

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