disjoint_cocompact_right — Mathlib

English

A filter is disjoint from cocompact iff it contains a compact set.

Русский

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

LaTeX

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

Lean4

/-- A filter is disjoint from the cocompact filter if and only if it contains a compact set. -/
theorem disjoint_cocompact_right (f : Filter X) : Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K :=
  by
  simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]
  tauto

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