Theorems · Theorem · combinatorics

Finset.sum_powerset_cons

∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β),
  ∑ t ∈ (Finset.cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (Finset.cons 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

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoid