prod_disjSum — Mathlib

English

For a finite sum type ι ⊕ κ, the product over the disjSum of a function f equals the product over the left side with Sum.inl and the right side with Sum.inr.

Русский

Для типа суммы ι ⊕ κ произведение по disjSum равно произведению по левой части и по правой части через Sum.inl и Sum.inr.

LaTeX

$$$\\prod_{x \\in s.\\text{disjSum}(t)} f(x) = \\left( \\prod_{x \\in s} f(Sum.inl x) \\right) \\left( \\prod_{x \\in t} f(Sum.inr x) \\right)$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_disjSum (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
    ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x) :=
  by
  rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
  rfl

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