Theorems · Theorem · combinatorics

Finset.inclusion_exclusion_sum_biUnion

• #96 of the 100 theorems: Principle of Inclusion/Exclusion

∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddCommGroup G] [inst_1 : DecidableEq α] (s : Finset ι)
  (S : ι → Finset α) (f : α → G), ∑ a ∈ s.biUnion S, f a = ∑ t, (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

Inclusion-exclusion principle for the sum of a function over a union. The sum of a function f over the union of the S i over i ∈ s is the alternating sum of the sums of f over the intersections of the S i.

Defined in

Mathlib.Combinatorics.Enumerative.InclusionExclusion

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupDecidableEq