prod_sum_eq_prod_toLeft_mul_prod_toRight

English

For a finite set s of sums ι ⊕ κ and function f, the product over s equals the product over its left projection and right projection separately.

Русский

Для конечного множества из суммы и функции f произведение равняется произведению по левой и правой частям отдельно.

LaTeX

$$$\\prod_{x \\in s} f(x) = \\left( \\prod_{x \\in s^{\\mathrm{toLeft}}} f(Sum.inl x) \\right) \\left( \\prod_{x \\in s^{\\mathrm{toRight}}} f(Sum.inr x) \\right)$$$

Lean4

@[to_additive]
theorem prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M) :
    ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) := by
  rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum, Finset.toRight_disjSum]

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