Theorems · Theorem · combinatorics

Finset.exists_card_fiber_lt_of_card_lt_mul

∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  s.card < t.card * n → ∃ y ∈ t, {x ∈ s | f x = y}.card < n

The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. ("The minimum is at most the mean" specialized to integers.) More formally, given a function f, a finite sets s in its domain, a finite set t in its codomain, and a natural number n such that #s < #t * n, there exists y ∈ t such that its preimage in s has less than n elements.

Defined in

Mathlib.Combinatorics.Pigeonhole

Cited by

0 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq