ite_prod_one — Mathlib

English

If p is a proposition, then ∏_{x∈s} (if p then 1 else f x) equals ∏_{x∈s} (f x) when p is false, and equals ∏_{x∈s} 1 when p is true.

Русский

Если p истинно, произведение равно ∏ 1, если ложно — ∏ f; т.е. существует разложение по условию.

LaTeX

$$$\\prod x \\in s, \\; \\mathrm{ite}\\; p \\; (1) \\; (f x) = \\mathrm{ite}\\; p \\; (\\prod x \\in s, 1) \\; (\\prod x \\in s, f x)$$$

Lean4

@[to_additive]
theorem ite_prod_one (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) :
    (if p then (∏ x ∈ s, f x) else 1) = ∏ x ∈ s, if p then f x else 1 := by simp only [prod_ite_irrel, prod_const_one]

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