Theorems · Theorem · combinatorics

Finset.sum_card_eq_sum_biUnion_card

∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (B : α → Finset β)
  (s : Finset α), ∑ j ∈ s, (B j).card = ∑ x ∈ s.biUnion B, {j | j ∈ s ∧ x ∈ B j}.card

Given a finite collection of finite subsets $B_1, \ldots, B_k$ and, for every $x \in \bigcup_i B_i$, let $C_x$ be the set of indices of the $B_i$'s that contain $x$. Then, $\sum_i |B_i| = \sum_x |C_x|$.

Defined in

Mathlib.Combinatorics.Enumerative.DoubleCounting

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidableEq