coprodᵢ_cofinite — Mathlib

English

For a finite index type ι, the indexed coproduct of cofinite filters equals the cofinite filter on the product.

Русский

Для конечного множества индексов ι копродукт кофинитных фильтров по i совпадает с кофинитным фильтром на произведении.

LaTeX

$$$(\text{finite } ι) \Rightarrow (\operatorname{coprod}ᵢ (\operatorname{cofinite} : \operatorname{Filter}(α_i)) = \operatorname{cofinite})$$$

Lean4

theorem coprodᵢ_cofinite {α : ι → Type*} [Finite ι] : (Filter.coprodᵢ fun i => (cofinite : Filter (α i))) = cofinite :=
  Filter.coext fun s => by simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

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