Theorems · Theorem · combinatorics

Finset.exists_card_fiber_lt_of_card_lt_nsmul

∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
  [inst_1 : CommSemiring M] [inst_2 : LinearOrder M] [IsStrictOrderedRing M],
  ↑s.card < t.card • b → ∃ y ∈ t, ↑{x ∈ s | f x = y}.card < b

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.

Defined in

Mathlib.Combinatorics.Pigeonhole

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiringLinearOrderIsStrictOrderedRing