English
Cardinality of the intersection of complements equals an alternating sum over intersections of the S_i's.
Русский
Кардинальность пересечения дополнений равна чередующейся сумме по пересечениям S_i.
LaTeX
$$$ \#\bigcap_{i\in s} S_i^c = \sum_{t\in s.powerset} (-1)^{|t|} \#(\bigcap_{i\in t} S_i) $$$
Lean4
/-- **Inclusion-exclusion principle** for the sum of a function over an intersection of complements.
The sum of a function `f` over the intersection of the complements of the `S i` over `i ∈ s` is the
alternating sum of the sums of `f` over the intersections of the `S i`. -/
theorem inclusion_exclusion_sum_inf_compl (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
classical
calc
∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
_ =
∑ t ∈ s.powerset.filter (¬·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a +
∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a :=
by
simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq', sub_eq_add_neg,
pow_succ]
_ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..
