mem_cocompact' — Mathlib

English

If s is compact, then its complement sᶜ belongs to cocompact X.

Русский

Если s компактно, то его дополнение sᶜ принадлежит кокомпактному фильтру.

LaTeX

$$$\operatorname{IsCompact}(s) \Rightarrow s^{c} \in \operatorname{cocompact}(X)$$$

Lean4

theorem mem_cocompact' : s ∈ cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t :=
  mem_cocompact.trans <| exists_congr fun _ => and_congr_right fun _ => compl_subset_comm

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