Theorems · Theorem · combinatorics

Finset.sum_powerset_insert

∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
  a ∉ s →
    ∀ (f : Finset α → β), ∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Cited by

2 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidDecidableEq