mem_cocompact — Mathlib

English

A set s belongs to cocompact X iff there exists a compact t with sᶜ ⊆ t.

Русский

Mножество принадлежит кокомпактному фильтру X тогда и только тогда, когда существует компактное t такое, что sᶜ ⊆ t.

LaTeX

$$$s \in \operatorname{cocompact}(X) \iff \exists t, \operatorname{IsCompact}(t) \land s^{c} \subseteq t$$$

Lean4

theorem mem_cocompact : s ∈ cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s :=
  hasBasis_cocompact.mem_iff

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