nonLindelofSpace_of_neBot

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

If Filter.coLindelof X is NeBot, then X is NonLindelofSpace.

Русский

Если Filter.coLindelof X не пуст, тогда X не Линдельфово.

LaTeX

$$$[\text{NeBot }(Filter.coLindelof X)] \Rightarrow NonLindelofSpace X$$$

Lean4

theorem nonLindelofSpace_of_neBot (_ : NeBot (Filter.coLindelof X)) : NonLindelofSpace X :=
  ⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_coLindelof).ne_empty compl_univ⟩

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

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

Разделы

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

Аффилиация

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