prod_piecewise — Mathlib

English

The product of a piecewise function over s equals the product over the intersection with the second set and the product over its complement.

Русский

Произведение по кусочно-заданной функции по s равно произведению по пересечению s и т и произведению по разности.

LaTeX

$$$\\prod_{x \\in s} (t.piecewise f g)(x) = \\left(\\prod_{x \\in s \\cap t} f(x)\\right) \\cdot \\left(\\prod_{x \\in s \\setminus t} g(x)\\right).$$$

Lean4

@[to_additive]
theorem prod_piecewise [DecidableEq ι] (s t : Finset ι) (f g : ι → M) :
    (∏ x ∈ s, (t.piecewise f g) x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x :=
  by
  simp only [piecewise]
  rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]

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