English
The alternating sum identity also holds for sums over complements: sum over intersections of complements equals a sum over all power-sets with appropriate signs.
Русский
Чередующаяся сумма также верна для сумм по пересечениям дополнений: сумма по пересечениям дополнений равна сумме по всем подмножествам с нужными знаками.
LaTeX
$$$ \sum_{a \in \bigcap_{i\in s} S_i^c} f(a) = \sum_{t \in s.powerset} (-1)^{|t|} \sum_{a \in \bigcap_{i\in t} S_i} f(a) $$$
Lean4
/-- **Inclusion-exclusion principle** for the cardinality of a union.
The cardinality of the union of the `S i` over `i ∈ s` is the alternating sum of the cardinalities
of the intersections of the `S i`. -/
theorem inclusion_exclusion_card_biUnion (s : Finset ι) (S : ι → Finset α) :
#(s.biUnion S) = ∑ t : s.powerset.filter (·.Nonempty), (-1 : ℤ) ^ (#t.1 + 1) * #(t.1.inf' (mem_filter.1 t.2).2 S) :=
by simpa using inclusion_exclusion_sum_biUnion (G := ℤ) s S (f := 1)
