prod_indicator_biUnion_finset_sub_indicator

English

The cardinality of a union is given by an alternating sum of cardinalities of intersections: #(s.biUnion S) = ∑_{t⊆s, t.Nonempty} (-1)^{|t|+1} #(t.inf' S).

Русский

Кардинальность объединения выражается чередующейся суммой кардинальностей пересечений: #(s.biUnion S) = ∑_{t⊆s, t.Nonempty} (-1)^{|t|+1} #(t.inf' S).

LaTeX

$$$ \#(s.biUnion S) = \sum_{t \in s.powerset, t.Nonempty} (-1)^{|t|+1} \#(t. inf' S) $$$

Lean4

theorem prod_indicator_biUnion_finset_sub_indicator (hs : s.Nonempty) (S : ι → Finset α) (a : α) :
    ∏ i ∈ s, (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) = (0 : ℤ) :=
  by
  convert prod_indicator_biUnion_sub_indicator hs (fun i ↦ S i) a
  simp

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