sum_powerset_neg_one_pow_card — Mathlib

English

Let X be a finite set. Then the sum over all subsets S of X of (-1)^{|S|} equals 1 if X is empty and 0 otherwise.

Русский

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

LaTeX

$$$$\sum_{S \subseteq X} (-1)^{|S|} = \begin{cases}1, & X = \emptyset,\\ 0, & X \neq \emptyset.\end{cases}$$$$

Lean4

theorem sum_powerset_neg_one_pow_card {α : Type*} [DecidableEq α] {x : Finset α} :
    (∑ m ∈ x.powerset, (-1 : ℤ) ^ #m) = if x = ∅ then 1 else 0 :=
  by
  rw [sum_powerset_apply_card]
  simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]

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