4.2 The principles of inclusion and exclusion
4.2.1 The size version
Let \(n \in \mathbb {N}\). Let \(U\) be a finite set. Let \(A_1, A_2, \ldots , A_n\) be \(n\) subsets of \(U\). Then,
Equivalently,
where \(\bigcap _{i \in I} A_i\) denotes \(\{ u \in U \mid u \in A_i \text{ for all } i \in I\} \) (so that \(\bigcap _{i \in \varnothing } A_i = U\)).
This is the inclusion-exclusion cardinality formula from Mathlib.
4.2.2 Alternative formulations of the size version
The complement of the union \(A_1 \cup A_2 \cup \cdots \cup A_n\) satisfies
This is the more common textbook formulation of the PIE.
Rewrite \((A_1 \cup \cdots \cup A_n)^c = \bigcap _i A_i^c\), then apply Theorem 4.43.
Let \(\alpha \) be a finite type and \(A_0, A_1, \ldots , A_{n-1}\) be \(n\) subsets of \(\alpha \) indexed by \(\{ 0, 1, \ldots , n{-}1\} \). Then
This is the specialization of Theorem 4.43 to the index set \(\{ 0, 1, \ldots , n{-}1\} \).
Given \(n\) “rules” encoded as subsets \(A_0, \ldots , A_{n-1}\) of a finite type \(\alpha \) (where \(A_i\) is the set of elements satisfying rule \(i\)), the number of elements violating all rules is
Rewrite both sides in terms of infima of complements and intersections, then apply Lemma 4.45.
4.2.3 Counting surjections
The number of surjective maps from \([m]\) to \([n]\) is defined as
- AlgebraicCombinatorics.InclusionExclusion.numSurj m n = Fintype.card { f : Fin m → Fin n // Function.Surjective f }
Let \(n, m \in \mathbb {N}\). Then,
A map \(f\colon [m] \to [n]\) is surjective if and only if it takes each \(i \in [n]\) as a value. Thus, imposing \(n\) rules on a map \(f\colon [m] \to [n]\), where rule \(i\) says “thou shalt not take \(i\) as a value,” the surjective maps are precisely the maps that violate all \(n\) rules. By the PIE (Theorem 4.43):
For each \(I \subseteq [n]\), the maps satisfying all rules in \(I\) are the maps from \([m]\) to \([n] \setminus I\), of which there are \((n - |I|)^m\). Substituting and splitting the sum by \(|I| = k\):
In Lean, we relate the surjection count to the PIE via the “avoid” sets \(S_i = \{ f \mid i \notin \operatorname {im} f\} \), apply the PIE (Theorem 4.43), substitute the cardinality formula for each subset, and rewrite the sum over the powerset as a sum over cardinalities.
Let \(m, n \in \mathbb {N}\) and let \(I\) be a subset of \([n]\). The number of functions \(f\colon [m] \to [n]\) such that \(i \notin \operatorname {im} f\) for all \(i \in I\) is \((n - |I|)^m\).
Such functions are exactly the functions from \([m]\) to \(I^c\), and \(|I^c| = n - |I|\).
For \(t \subseteq [n]\), the cardinality of the intersection \(\bigcap _{i \in t} S_{\mathrm{avoid}}(i)\) is \((n - |t|)^m\), where \(S_{\mathrm{avoid}}(i) = \{ f\colon [m] \to [n] \mid i \notin \operatorname {im} f\} \).
The intersection equals the set of functions whose range avoids all elements of \(t\), which by Lemma 4.49 has cardinality \((n - |t|)^m\).
4.2.4 Consequences of the surjection formula
Let \(n \in \mathbb {N}\). Then:
(a) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m = 0\) for any \(m \in \mathbb {N}\) satisfying \(m {\lt} n\).
(b) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^n = n!\).
(c) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m \geq 0\) for each \(m \in \mathbb {N}\).
(d) We have \(n! \mid \sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m\) for each \(m \in \mathbb {N}\).
(a) By Theorem 4.48, the sum equals the number of surjective maps \(f\colon [m] \to [n]\). Since \(m {\lt} n\), no such surjection exists (by the Pigeonhole Principle), so the sum is \(0\).
(b) By Theorem 4.48 with \(m = n\), the sum counts surjections \(f\colon [n] \to [n]\), which are precisely the permutations of \([n]\), of which there are \(n!\).
(c) The sum equals the number of surjections, which is a nonnegative integer.
(d) The symmetric group \(S_n\) acts on the set \(U := \{ \text{surjective maps } f\colon [m] \to [n]\} \) by post-composition (\(\sigma \cdot f = \sigma \circ f\)). This action is free: if \(\sigma \circ f = f\) and \(f\) is surjective, then for each \(j \in [n]\), pick \(i\) with \(f(i) = j\); then \(\sigma (j) = \sigma (f(i)) = f(i) = j\), so \(\sigma = \mathrm{id}\) (Lemma 4.54). By the orbit–stabilizer theorem, each orbit has size \(n!\), so the orbits partition \(U\) into blocks of size \(n!\), whence \(n! \mid |U|\) (Lemma 4.55).
4.2.5 Helpers for the divisibility proof
If \(\sigma \) is a permutation of \([n]\) and \(f\colon [m] \to [n]\) is surjective, then \(\sigma \circ f\) is surjective.
Given \(y \in [n]\), since \(f\) is surjective there exists \(x\) with \(f(x) = \sigma ^{-1}(y)\), so \(\sigma (f(x)) = y\).
The symmetric group \(S_n\) acts on the set of surjective functions \(f\colon [m] \to [n]\) by post-composition: \(\sigma \cdot f := \sigma \circ f\).
- One or more equations did not get rendered due to their size.
Well-definedness follows from Lemma 4.52. The action laws \(1 \cdot f = f\) and \((\sigma \tau ) \cdot f = \sigma \cdot (\tau \cdot f)\) are immediate from composition.
Let \(f\colon [m] \to [n]\) be surjective. Then the stabilizer of \(f\) under the action of \(S_n\) by post-composition is trivial.
If \(\sigma \circ f = f\) and \(f\) is surjective, then for each \(y \in [n]\), pick \(x\) with \(f(x) = y\); then \(\sigma (y) = \sigma (f(x)) = f(x) = y\). So \(\sigma = \mathrm{id}\).
We have \(n! \mid \mathrm{numSurj}(m, n)\).
By the orbit–stabilizer theorem, each orbit of the free action of \(S_n\) on surjections has size \(|S_n|/|\{ \mathrm{id}\} | = n!\), so the orbits partition the set of surjections into blocks of size \(n!\).
4.2.6 Derangements
A derangement of a set \(X\) means a permutation of \(X\) that has no fixed points.
- AlgebraicCombinatorics.InclusionExclusion.Derangement α = { σ : Equiv.Perm α // ∀ (x : α), σ x ≠ x }
We write \(D_n\) for the number of derangements of \([n]\).
The set of derangements of \(\alpha \) (as defined in Definition 4.56) is in bijection with the set of fixed-point-free permutations from Mathlib.
- One or more equations did not get rendered due to their size.
Both are defined by the same predicate (having no fixed points) on the set of permutations of \(\alpha \).
The identity permutation is a derangement of the empty type (vacuously, it has no fixed points). Hence \(D_0 = 1\).
Since the type is empty, there are no elements to be fixed points.
If \(\alpha \) is nonempty, then no derangement of \(\alpha \) equals the identity permutation. In particular \(D_1 = 0\).
If \(d\) is a derangement with \(d = \mathrm{id}\), pick any \(x \in \alpha \); then \(d(x) = x\), contradicting the fixed-point-free property.
The first few values of the derangement count are: \(D_2 = 1\) (the only derangement of \(\{ 0,1\} \) is the swap) and \(D_3 = 2\) (the two \(3\)-cycles).
By computation (verified by decision procedure in Lean).
The number of derangements of \([n]\) (as defined in Definition 4.56) agrees with Mathlib’s derangement count.
Follows from Lemma 4.57 and Mathlib’s computation of the derangement count.
Let \(n \in \mathbb {N}\). Then, the number of derangements of \([n]\) is
Set \(U := S_n\) (the set of all permutations of \([n]\)). Impose \(n\) rules \(1, 2, \ldots , n\) on a permutation \(\sigma \in U\), with rule \(i\) being “thou shalt leave the element \(i\) fixed” (i.e., rule \(i\) requires \(\sigma (i) = i\)). Derangements are precisely the permutations violating all \(n\) rules. By the PIE (Theorem 4.43):
For each \(I \subseteq [n]\), the permutations satisfying all rules in \(I\) are the permutations of \([n]\) that leave each \(i \in I\) fixed; there are \((n - |I|)!\) such permutations (they are essentially the permutations of the \((n - |I|)\)-element set \([n] \setminus I\)). Substituting and grouping by \(|I| = k\):
In Lean, the first equality is derived from Mathlib’s derangement sum formula using the identity \((n-k)! \cdot \binom {n}{k} = n!/k!\).
Let \(n \in \mathbb {N}\). Then,
(This is the same formula as in Theorem 4.62, but stated over \(\mathbb {Q}\) so that the division \(1/k!\) is literal.)
Convert Theorem 4.62 from \(\mathbb {Z}\) to \(\mathbb {Q}\), then use \(\binom {n}{k} (n-k)! = n!/k!\).
4.2.7 Euler’s totient formula
Let \(c\) be a positive integer with prime factorization \(p_1^{a_1} p_2^{a_2} \cdots p_n^{a_n}\), where \(p_1, p_2, \ldots , p_n\) are distinct primes and \(a_1, a_2, \ldots , a_n\) are positive integers. Then,
A number \(u \in [c]\) is coprime to \(c\) if and only if it is not divisible by any of the prime factors \(p_1, \ldots , p_n\) of \(c\). Thus \(u\) must break all \(n\) rules \(1, 2, \ldots , n\), where rule \(i\) says “thou shalt be divisible by \(p_i\).” By the PIE (Theorem 4.43):
(The factorization of the sum over subsets into a product uses the identity \(\sum _{I \subseteq [n]} \prod _{i \in I} x_i = \prod _{i=1}^{n}(1 + x_i)\).)
In Lean, this is derived from Mathlib’s totient formula.
4.2.8 The weighted version
Let \(n \in \mathbb {N}\), and let \(U\) be a finite set. Let \(A_1, A_2, \ldots , A_n\) be \(n\) subsets of \(U\). Let \(G\) be any additive abelian group. Let \(w\colon U \to G\) be any map. Then,
This is the weighted inclusion-exclusion formula from Mathlib.
Let \(U\) be a finite set, \(s\) a finite index set, \(A_i\) subsets of \(U\) for \(i \in s\), \(G\) an additive abelian group, and \(w\colon U \to G\) a weight function. Then,
Specialization of Theorem 4.65 to an explicit index set.
The size version of the PIE (Theorem 4.43) follows from the weighted version (Theorem 4.65) by taking the weight function \(w(u) = 1\) for all \(u\). Explicitly, for a finite type \(U\), finite index set \(s\), and subsets \(A_i\) of \(U\):
Specialize Theorem 4.66 to \(G = \mathbb {Z}\) and \(w \equiv 1\). Each weighted sum \(\sum _{u \in S} w(u) = \sum _{u \in S} 1 = |S|\).