coprod_cofinite — Mathlib

English

The coproduct of the cofinite filters on two types is the cofinite filter on their product.

Русский

Копродукт кофинитных фильтров на двух множествах равен кофинитному фильтру на их произведении.

LaTeX

$$$(\operatorname{cofinite} : \operatorname{Filter} \alpha)\operatorname{coprod}(\operatorname{cofinite} : \operatorname{Filter} \beta) = \operatorname{cofinite}$$$

Lean4

/-- The coproduct of the cofinite filters on two types is the cofinite filter on their product. -/
theorem coprod_cofinite : (cofinite : Filter α).coprod (cofinite : Filter β) = cofinite :=
  Filter.coext fun s => by simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

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