prod_mul_prod — Mathlib

English

If s and t form a complement (IsCompl s t) in a finite index set, then the product over s times the product over t equals the product over all indices.

Русский

Если s и t образуют дополнение (IsCompl s t) в конечном множестве индексов, то произведение по s и по t равно произведению по всем индексам.

LaTeX

$$$IsCompl(s,t) \\Rightarrow \\left( \\prod_{i \\in s} f(i) \\right) \\left( \\prod_{i \\in t} f(i) \\right) = \\prod_{i} f(i)$$$

Lean4

@[to_additive]
theorem _root_.IsCompl.prod_mul_prod [Fintype ι] {s t : Finset ι} (h : IsCompl s t) (f : ι → M) :
    (∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i, f i :=
  (Finset.prod_disjUnion h.disjoint).symm.trans <| by
    classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

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