Skip to content
Axiomatic Wiki
Theorem·T12

The pigeonhole principle

More pigeons than holes: some hole gets two pigeons.

For all with , there is no injective function Equivalently: however objects are assigned to boxes with , two objects share a box. Order from D029.
In words
For any natural numbers n and m with n strictly smaller than m, there is no one-to-one function from m to n: m objects cannot be assigned to n boxes without two sharing a box.
Rests onF02F03F04F06F08F09F11F14A01A06A08
Never needed: F05 · F10 · F12 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    We prove by induction on that no injective function maps any into : let a set by Separation.
  2. 2
    Base, : let and suppose is a function. Since means (D029), the value would be a member of , which has none (D002, D013). So no function exists at all, let alone an injective one (negation).
  3. 3
    Step: assume ; suppose toward a contradiction that and is injective. Since , , so for some by L15 (vii). From : by L15 (iii), and by (vi), so by transitivity (ii) (the case via substitutivity).
  4. 4
    Note (as by (vi)), so is defined; and every has (by transitivity of the natural , L07). Define with domain by the swap rule: a set by Separation inside , and a function since exactly one clause applies to each (excluded middle).
  5. 5
    lands in : for the first clause, and force (D006, D003). For the second clause: if with , then , because is injective and (indeed and is impossible by L15 (i)); hence by the same successor analysis.
  6. 6
    is injective: let with . If both used the first clause: , so by injectivity of . Both on the second clause: , so again . Mixed, say and : then and , so , and injectivity of gives ; but , contradicting (L15 (i)). So the mixed case cannot occur (case analysis).
  7. 7
    Thus is injective with , contradicting the induction hypothesis . Hence no injective exists, , and T05 gives .
∎

Remarks

Dirichlet's box principle (1834), here in its exact finite form. The swap rule in the proof is the whole trick: to shrink an injection to one , redirect the one argument that hits the top value to the value of the discarded top argument . Immediate consequences: distinct naturals are never equinumerous (a bijection would inject the larger into the smaller), which is uniqueness of cardinality; and no finite set matches a proper subset of itself. Applications are everywhere: two Londoners have the same number of hairs; any numbers from contain a divisor pair; every rational's decimal expansion repeats.
Wikipedia ↗Fintype.card_le_of_injective ↗

Used by

L23L33T20
Propose an edit1 published revision