prod_ite — Mathlib

English

If for every i ∈ s, p(i) is false, then the product of the dite expression equals the product of the g-part over s.

Русский

Если для всех i∈s выполняется p(i) = ложь, то произведение dite равно произведению g(i).

LaTeX

$$$\\prod_{i \\in s} (\\text{if } p(i) \\text{ then } f(i) \\text{ else } g(i)) = \\prod_{i \\in s} g(i).$$$

Lean4

@[to_additive]
theorem prod_ite {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → M) :
    ∏ x ∈ s, (if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x := by
  simp [prod_apply_ite _ _ fun x => x]

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