English
For a,b in a commutative semiring and a finite index set ι, the sum of a^{|s|} b^{|ι|-|s|} over all subsets s⊆ι equals (a+b)^{|ι|}. (A version labeled in the Fintype namespace states the same with univ).
Русский
Для конечного множества ι и элементов a,b в коммутативной полугруппе верно: сумма по всем подмножествам s⊆ι от a^{|s|} b^{|ι|-|s|} равна (a+b)^{|ι|}.
LaTeX
$$$\\sum_{s\\subseteq \\iota} a^{|s|} b^{|\\iota|-|s|} = (a+b)^{|\\iota|}$$$
Lean4
/-- `∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j)`. This formula is useful in construction of
a partition of unity from a collection of “bump” functions. -/
theorem prod_one_sub_ordered [LinearOrder ι] (s : Finset ι) (f : ι → R) :
∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j) :=
by
rw [prod_sub_ordered]
simp
