cocompact_le_coclosedCompact

Mathlib.Topology.Compactness.Compact

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

English

Cocompact filter is below coclosedCompact filter.

Русский

Кокомпактность фильтра ⊆ коклosedCompact

LaTeX

$$$\operatorname{cocompact}(X) \le \operatorname{coclosedCompact}(X)$$$

Lean4

theorem cocompact_le_coclosedCompact : cocompact X ≤ coclosedCompact X :=
  iInf_mono fun _ => le_iInf fun _ => le_rfl

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

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

Разделы

Аффилиация

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