English
The cofinite filter on α has as a basis the complements of finite subsets: for every finite s, α \ s ∈ cofinite, and conversely, any cofinite set contains some α \ s with s finite.
Русский
У кофинитного фильтра на α базисом служат дополнения конечных подмножеств: для каждого конечного s множества α \ s ∈ cofinite, и наоборот, любой кофинитный набор содержит некоторое α \ s с конечным s.
LaTeX
$$$\{\alpha \setminus s \mid s \subseteq \alpha,\ s \text{ finite}\}$ является базисом для $\operatorname{cofinite}$$$
Lean4
theorem hasBasis_cofinite : HasBasis cofinite (fun s : Set α => s.Finite) compl :=
⟨fun s => ⟨fun h => ⟨sᶜ, h, (compl_compl s).subset⟩, fun ⟨_t, htf, hts⟩ => htf.subset <| compl_subset_comm.2 hts⟩⟩
