Alphabeta Math

Inclusion–Exclusion, the Pigeonhole Principle and Double Counting

About this page
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 15 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Combinatorics
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Lemma

∑_i ∈ S∑_j ∈ T aᵢⱼ = ∑_(i,j) ∈ S × T aᵢⱼ = ∑_j ∈ T∑_i ∈ S aᵢⱼ for finite index sets S and T

Definition

A relation R ⊆ X × Y between finite sets, its row fibres Rₓ and its column fibres Rʸ

Theorem

Double counting: ∑_x ∈ X| Rₓ| = | R| = ∑_y ∈ Y| Rʸ| for a relation between finite sets

Corollary

If X is nonempty, some row fibre is at least the average size and some row fibre is at most the average size

Definition

⌈ m/n ⌉ for naturals m and n ≥ 1: the least q ∈ ℕ with m ≤ n q

Theorem

If | A| > k| B| then every f : A → B has a fibre with more than k elements, and for nonempty B some fibre has at least ⌈ | A| / | B|⌉ elements

Definition

A finite family (Aᵢ)_i ∈ I of subsets of a finite set X, the intersections A_J for J ⊆ I, and the convention A_∅ = X

Theorem

Inclusion and exclusion: ι|⋃_i ∈ I Aᵢ| = ∑_∅ ≠ J ⊆ I(-1)^| J| + 1 ι| A_J|, together with the complementary form counting the elements in none of the Aᵢ

Lemma

∑_j<m+1(-1)ʲ iotaC(t, j) = (-1)ᵐ iotaC(t-1, m) for every t ≥ 1 and every m

Theorem

Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it

Theorem

The number of surjections from an n-element set onto a k-element set is ∑_i<k+1(-1)ⁱC(k, i)(k-i)ⁿ, read in ℝ through ι

Definition

The derangement number Dₙ: the number of bijections of an n-element set with no fixed point

Theorem

ι(Dₙ) = ι(n!)∑_i<n+1(-1)ⁱ/ι(i!), with the term at i = 0 equal to 1 and D₀ = 1

Corollary

ι(Dₙ) = ι(n) ι(Dₙ₋₁) + (-1)ⁿ for n ≥ 1, and Dₙ = (n-1)(Dₙ₋₁ + Dₙ₋₂) for n ≥ 2

Definition

A finite list of reals, and its strictly increasing and strictly decreasing sublists

Theorem

Every list of mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1 or a strictly decreasing sublist of length n+1

Theorem

For all m and n there is a list of mn pairwise distinct reals with no strictly increasing sublist of length m+1 and no strictly decreasing sublist of length n+1

Remark

The conventions this page fixes: the empty intersection, where the counts live, the first index of every sum, and what the declared prerequisites do not supply

False statement

FALSE: the real-valued three-set inclusion-exclusion identity remains true after deleting the triple-intersection term

False statement

FALSE: truncating the sieve at a fixed depth of at least two gives the exact size of the union

False statement

FALSE: every list of mn pairwise distinct reals has a strictly increasing sublist of length m+1 or a strictly decreasing sublist of length n+1

Sources