English
The sum over the union equals an alternating sum over intersections: ∑ a∈⋃_{i∈s} S_i f(a) = ∑_{t⊆s, t≠∅} (-1)^{|t|+1} ∑_{a∈⋂_{i∈t} S_i} f(a).
Русский
Сумма по объединению равна чередующейся сумме по пересечениям: ∑_{a∈⋃_{i∈s} S_i} f(a) = ∑_{t⊆s, t≠∅} (-1)^{|t|+1} ∑_{a∈⋂_{i∈t} S_i} f(a).
LaTeX
$$$ \sum_{a\in \bigcup_{i\in s} S_i} f(a) = \sum_{t\in s.powerset, t.Nonempty} (-1)^{|t|+1} \sum_{a\in \bigcap_{i\in t} S_i} f(a) $$$
Lean4
/-- **Inclusion-exclusion principle**, indicator version over a finite union of sets. -/
theorem indicator_biUnion_eq_sum_powerset (s : Finset ι) (S : ι → Set α) (f : α → G) (a : α) :
Set.indicator (⋃ i ∈ s, S i) f a =
∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a :=
by
classical
by_cases ha : a ∈ ⋃ i ∈ s, S i; swap
· simp only [ha, not_false_eq_true, Set.indicator_of_notMem, Int.reduceNeg, pow_succ, mul_neg, mul_one, neg_smul]
symm
apply sum_eq_zero
simp only [Int.reduceNeg, neg_eq_zero, mem_filter, mem_powerset, and_imp]
intro t hts ht
rw [Set.indicator_of_notMem]
· simp
· contrapose! ha
simp only [Set.mem_iInter] at ha
rcases ht with ⟨i, hi⟩
simp only [Set.mem_iUnion, exists_prop]
exact ⟨i, hts hi, ha _ hi⟩
rw [← sub_eq_zero]
calc
Set.indicator (⋃ i ∈ s, S i) f a -
∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • Set.indicator (⋂ i ∈ t.1, S i) f a
_ =
∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a +
∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a :=
by simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ, ha]
_ = ∑ t ∈ s.powerset, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a := by rw [sum_filter_add_sum_filter_not]
_ = (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a :=
by
simp only [Int.reduceNeg, prod_sub, prod_const_one, mul_one, sum_smul]
congr! 1 with t
simp only [prod_const_one, prod_indicator_apply]
simp [Set.indicator]
_ = 0 := by
have : Set.indicator (⋃ i ∈ s, S i) 1 a = (1 : ℤ) := Set.indicator_of_mem ha 1
rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]
simp only [Set.mem_iUnion, exists_prop] at ha
rcases ha with ⟨i, hi, -⟩
exact ⟨i, hi⟩
