Pigeonhole principles

TheoremFinite#

The pigeonhole principle for finitely many pigeons and pigeonholes. This is the Fintype version of Finset.exists_ne_map_eq_of_card_lt_of_maps_to.

Fintype.exists_ne_map_eq_of_card_lt.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β]
  (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y
Sources
MathlibFintype.exists_ne_map_eq_of_card_lt
Uses 2 · Used by 1
Statement usesFinite set · Natural number
Used byTurán's theorem

TheoremInfinite#

The strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there is a pigeonhole with infinitely many pigeons.

See also: Finite.exists_ne_map_eq_of_infinite

Finite.exists_infinite_fiber.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β]
  (f : α → β) : ∃ y, Infinite ↑(f ⁻¹' {y})
Sources
MathlibFinite.exists_infinite_fiber
Uses 2
Statement usesNatural number
Proof usesFinite set

TheoremStrong pigeonhole principle#

The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. ("The maximum is at least the mean" specialized to integers.)

More formally, given a function f between finite types α and β and a number n such that card β * n < card α, there exists an element y : β such that its preimage has more than n elements.

Fintype.exists_lt_card_fiber_of_mul_lt_card.{u, v} {α : Type u} {β : Type v} [DecidableEq β]
  [Fintype α] [Fintype β] (f : α → β) {n : ℕ} (hn : Fintype.card β * n < Fintype.card α) :
  ∃ y, n < {x | f x = y}.card
Sources
MathlibFintype.exists_lt_card_fiber_of_mul_lt_card
Uses 2
Statement usesFinite set · Natural number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.