prod_one_add — Mathlib

English

For any finite set s and function f: i ↦ R, the product over i∈s of (1 + f(i)) equals the sum over t∈powerset(s) of the product over i∈t of f(i).

Русский

Для конечного множества s и функции f: i → R, произведение (1+f(i)) по i∈s равно сумма по всем подмножествам t множества s от произведения f(i) по i∈t.

LaTeX

$$$\\prod_{i\\in s} (1 + f(i)) = \\sum_{t \\in s.powerset} \\prod_{i\\in t} f(i)$$$

Lean4

theorem prod_one_add {f : ι → R} (s : Finset ι) : ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i := by
  classical simp only [add_comm (1 : R), prod_add, prod_const_one, mul_one]

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