noncompactSpace_of_neBot

Mathlib.Topology.Compactness.Compact

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

← MathLib Explorer

English

If the cocompact filter on X is NeBot, then X is a noncompact space.

Русский

Если cocompact фильтр на X не тривиален, то X не компактно.

LaTeX

$$NoncompactSpace X$$

Lean4

theorem noncompactSpace_of_neBot (_ : NeBot (Filter.cocompact X)) : NoncompactSpace X :=
  ⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_cocompact).ne_empty compl_univ⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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