prod_compl_mul_prod — Mathlib

English

Same as the previous lemma with corollaries for a finite index set; the complement and the original sets multiply to give the full product.

Русский

То же, что и предыдущее свойство, с выводами для конечного множества индексов; дополнение и исходные множества перемножаются в полное произведение.

LaTeX

$$$\\left( \\prod_{i \\in s^{c}} f(i) \\right) \\left( \\prod_{i \\in s} f(i) \\right) = \\prod_{i} f(i)$$$

Lean4

@[to_additive]
theorem prod_compl_mul_prod [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
    (∏ i ∈ sᶜ, f i) * ∏ i ∈ s, f i = ∏ i, f i :=
  (@isCompl_compl _ s _).symm.prod_mul_prod f

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