sum_powerset_neg_one_pow_card_of_nonempty

English

If X is a nonempty finite set, then the alternating sum over all subsets S ⊆ X of (-1)^{|S|} is 0.

Русский

Если X — непустое конечное множество, то чередующаяся сумма по всем подмножествам S ⊆ X от (-1)^{|S|} равна 0.

LaTeX

$$$$\sum_{S \subseteq X} (-1)^{|S|} = 0 \quad \text{whenever } X \neq \emptyset.$$$$

Lean4

theorem sum_powerset_neg_one_pow_card_of_nonempty {α : Type*} {x : Finset α} (h0 : x.Nonempty) :
    (∑ m ∈ x.powerset, (-1 : ℤ) ^ #m) = 0 := by
  classical
  rw [sum_powerset_neg_one_pow_card]
  exact if_neg (nonempty_iff_ne_empty.mp h0)

Похожие утверждения