English
If |s| < |t| · n for finite sets s into t with a function f: s → t, then there exists y ∈ t with the fiber {x ∈ s | f(x) = y} having size less than n.
Русский
Если |s| < |t| · n, то существует y ∈ t такое, что фойбер {x ∈ s | f(x) = y} имеет размер менее чем n.
LaTeX
$$$\\exists y \\in t, \\#\\{x \\in s \\mid f(x) = y\\} < n$$$
Lean4
/-- 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. -/
theorem exists_card_fiber_lt_of_card_lt_mul (hn : #s < #t * n) : ∃ y ∈ t, #({x ∈ s | f x = y}) < n :=
exists_card_fiber_lt_of_card_lt_nsmul hn
