cocompact_le_cofinite — Mathlib

English

The cocompact filter is below the cofinite filter; i.e., every cocompact set is cofinite.

Русский

Кокомпактный фильтр находится ниже кофиничного фильтра; то есть каждое множество из кокомпактного фильтра — кофайн.

LaTeX

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

Lean4

theorem cocompact_le_cofinite : cocompact X ≤ cofinite := fun s hs => compl_compl s ▸ hs.isCompact.compl_mem_cocompact

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