coclosedCompact — Mathlib

English

CoclosedCompact is the filter generated by complements to closed compact sets; in a Hausdorff space, this equals cocompact.

Русский

CoclosedCompact — фильтр, порожденный дополнениями к замкнутым компакт-множества; в пространстве Хаусдорфа это равно cocompact.

LaTeX

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

Lean4

/-- `Filter.coclosedCompact` is the filter generated by complements to closed compact sets.
In a Hausdorff space, this is the same as `Filter.cocompact`. -/
def coclosedCompact : Filter X :=
  ⨅ (s : Set X) (_ : IsClosed s) (_ : IsCompact s), 𝓟 sᶜ

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