Inclusion-Exclusion Principle

Statement

For finite sets $A_1, \ldots, A_n$:

For the two-set case this simplifies to:

Visualization

Venn diagram — two overlapping sets of integers:

    Set A                Set B
  ┌──────────┐        ┌──────────┐
  │  2  4  6 │  8 10  │ 10 15 20 │
  │          │◄──────►│          │
  │          │ 8, 10  │          │
  └──────────┘        └──────────┘

Let $A = \{2, 4, 6, 8, 10\}$ and $B = \{8, 10, 15, 20\}$.

Quantity	Value	Count
$A$	$\{2, 4, 6, 8, 10\}$	5
$B$	$\{8, 10, 15, 20\}$	4
$A \cap B$	$\{8, 10\}$	2
$A \cup B$	$\{2, 4, 6, 8, 10, 15, 20\}$	7

Formula check: $5 + 4 - 2 = 7$. Correct.

Three-set example — students taking courses:

         Math (M)
        ┌───────────────┐
        │   5           │
        │  ┌──────┐     │
        │  │ 3    │  2  │
        │  │  ┌───┼──┐  │
        │  │  │ 1 │  │  │
        │  └──┼───┘  │  │
        └─────┼──────┘  │
   CS (C)     │  Physics (P)
              └──────────┘

$|M|=12,\; |C|=10,\; |P|=8,\; |M\cap C|=4,\; |M\cap P|=3,\; |C\cap P|=2,\; |M\cap C\cap P|=1$.

Proof Sketch

The key observation: each element $x \in A_{i_1} \cap \cdots \cap A_{i_k}$ (belonging to exactly $k$ of the sets) is counted $\binom{k}{1} - \binom{k}{2} + \cdots + (-1)^{k+1}\binom{k}{k}$ times in the alternating sum. By the binomial theorem, this equals $1 - (1-1)^k = 1$. So every element is counted exactly once. $\square$

For the two-set case: draw the Venn diagram, observe elements in $A \cap B$ are double-counted in $|A| + |B|$, and subtract once.

Connections

• Pigeonhole PrinciplePigeonhole Principle$$|f^{-1}(\{y\})| \geq 2 \;\text{for some}\; y \in B \;\text{when}\; |A| > |B|$$If n+1 objects are placed into n boxes, some box contains at least two objectsRead more → — a crude cousin: forces existence of a collision without counting precisely
• Catalan NumbersCatalan Numbers$$C_n = \frac{1}{n+1}\binom{2n}{n}$$The ubiquitous sequence counting balanced parentheses, binary trees, and Dyck pathsRead more → — the ballot problem uses complementary counting, an inclusion-exclusion variant
• Stirling NumbersStirling Numbers$$S(n,k) = k \cdot S(n-1,k) + S(n-1,k-1)$$Counting partitions of n elements into k non-empty subsetsRead more → — the explicit formula for $S(n,k)$ involves an inclusion-exclusion sum over $k$
• Bell NumbersBell Numbers$$B_n = \sum_{k=0}^{n} S(n, k)$$The total number of partitions of a set of n elementsRead more → — $B_n = \sum_k S(n,k)$ accumulates Stirling numbers, each built on inclusion-exclusion
• Möbius InversionMöbius Inversion$$f(n) = \sum_{d \mid n} \mu(d)\, g\!\left(\frac{n}{d}\right)$$If g equals the Dirichlet convolution of f with the constant 1, then f recovers via the Möbius functionRead more → — the Möbius function on a poset is the categorical generalization of inclusion-exclusion
• Fermat's Little TheoremFermat's Little Theorem$$a^p \equiv a \pmod{p}$$For prime p, a^p is congruent to a mod pRead more → — Euler's totient $\phi(n)$ is computed via inclusion-exclusion on prime factors

import Mathlib.Data.Finset.Basic

/-- Two-set inclusion-exclusion: |A ∪ B| = |A| + |B| - |A ∩ B|.
    Proved from `Finset.card_union_add_card_inter` using `omega`. -/
theorem inc_exc_two {α : Type*} [DecidableEq α] (s t : Finset α) :
    (s ∪ t).card = s.card + t.card - (s ∩ t).card := by
  have h := Finset.card_union_add_card_inter s t
  omega

/-- The additive form is already in Mathlib as `Finset.card_union_add_card_inter`:
    |(s ∪ t)| + |s ∩ t| = |s| + |t|. -/
theorem inc_exc_additive {α : Type*} [DecidableEq α] (s t : Finset α) :
    (s ∪ t).card + (s ∩ t).card = s.card + t.card :=
  Finset.card_union_add_card_inter s t

/-- Concrete check: {1,2,3} ∪ {2,3,4} has cardinality 4. -/
theorem inc_exc_example :
    ({1, 2, 3} ∪ {2, 3, 4} : Finset ℕ).card = 4 := by decide