Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Combinatorics

Pigeonhole Principle

Map a larger finite collection into a smaller finite collection. At least two distinct inputs must land on the same output.

Exact theorem

Exact Mathlib statement

theorem Fintype.exists_ne_map_eq_of_card_lt {α β : Type*} [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y

The theorem at a glance

Pigeonhole principle at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

A function from a larger finite type to a smaller finite type must identify at least two distinct inputs. Explanatory diagram.
Detailed visual description

The poster leads with f : α → β, the exact condition Fintype.card β < Fintype.card α, and the conclusion ∃ x y, x ≠ y ∧ f x = f y. A representative seven-to-four map uses distinct patterns for source objects and emphasizes two selected inputs whose threads meet at the same target. The lower route follows the checked proof through the two full finite universes and the finite-set collision theorem, while the footer excludes uniqueness, a fiber-size bound, and an infinite variant.

Statement structure

From hypotheses to conclusion

Statement map for Pigeonhole PrincipleA function from a larger finite type to a smaller one has two distinct inputs with the same image. The pinned upstream declaration is Fintype.exists_ne_map_eq_of_card_lt. The exact checked statement is theorem Fintype.exists_ne_map_eq_of_card_lt {α β : Type*} [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y.Mathematical readingA function from a largerfinite type to a smallerone has two distinctinputs with the sameimage.Pinned declarationmathlib ·Fintype.exists_ne_map_eq_of_card_ltExact checked formtheoremFintype.exists_ne_map_eq_of_card_lt{α β : Type*} [Fintypeα] [Fintype β] (f : α →β) (h : Fintype.card β <Fintype.card α) : ∃ x y,x ≠ y ∧ f x = f yStatement map for Pigeonhole PrincipleA function from a larger finite type to a smaller one has two distinct inputs with the same image. The pinned upstream declaration is Fintype.exists_ne_map_eq_of_card_lt. The exact checked statement is theorem Fintype.exists_ne_map_eq_of_card_lt {α β : Type*} [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y.Mathematical readingA function from a largerfinite type to a smallerone has two distinctinputs with the sameimage.Pinned declarationmathlib ·Fintype.exists_ne_map_eq_of_card_ltExact checked formtheoremFintype.exists_ne_map_eq_of_card_lt{α β : Type*} [Fintypeα] [Fintype β] (f : α →β) (h : Fintype.card β <Fintype.card α) : ∃ x y,x ≠ y ∧ f x = f y

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Seven mapped source elements force a collision among four available targets; the textured pair highlights one witness while one target remains unoccupied. Explanatory scientific diagram.
Detailed visual description

A rounded source field contains exactly seven vertically arranged tokens and a smaller target field contains exactly four chambers. Exactly seven threads leave the source tokens. The top three charcoal threads meet the top cobalt chamber. Separate gold threads from one striped token and one dotted token meet the second emerald chamber. Two lower charcoal threads meet the third muted-vermilion chamber. The outlined bottom chamber has no incident thread, so the composition does not imply surjectivity.

Why it matters

A mathematical landmark

The pigeonhole principle is one of the most basic and reusable existence arguments in discrete mathematics. Mathlib's selected declaration captures its exact finite-type core and derives it directly from the corresponding finite-set collision theorem on the two full universes.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's weak finite-type pigeonhole principle. For [Fintype α], [Fintype β], f : α → β, and Fintype.card β < Fintype.card α, the selected declaration supplies x and y with x ≠ y and f x = f y. It asserts one collision, not a unique or canonical pair, a quantitative lower bound on a fiber, the strong infinite-fiber principle, surjectivity, or an arbitrary-cardinal theorem.

Source and local evidence

Where the theorem comes from

Existing declaration
Fintype.exists_ne_map_eq_of_card_lt in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.pigeonhole-principle.v001
Source
Open the pinned upstream reference