compl_mem_cocompact — Mathlib

English

A filter is disjoint from the cocompact filter if and only if it contains a compact set.

Русский

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

LaTeX

$$$\operatorname{Disjoint}(\operatorname{cocompact}(X), f) \iff \exists K \in f, \operatorname{IsCompact}(K)$$$

Lean4

theorem _root_.IsCompact.compl_mem_cocompact (hs : IsCompact s) : sᶜ ∈ Filter.cocompact X :=
  hasBasis_cocompact.mem_of_mem hs

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