disjoint_cocompact_left — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{Disjoint}(\operatorname{cocompact}(X), f) \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_left (f : Filter X) : Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K :=
  by
  simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]
  tauto

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