cocompact — Mathlib

English

Filter cocompact is the infimum of principal filters of complements to compact sets: ⨅ s IsCompact s, 𝓟 sᶜ.

Русский

Фильтр cocompact есть инфимум принципиев над дополнениями компактов: ⨅ s IsCompact s, 𝓟 sᶜ.

LaTeX

$$def cocompact : Filter X := ⨅ (s : Set X) (_ : IsCompact s), 𝓟 sᶜ$$

Lean4

/-- `Filter.cocompact` is the filter generated by complements to compact sets. -/
def cocompact : Filter X :=
  ⨅ (s : Set X) (_ : IsCompact s), 𝓟 sᶜ

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