English
There exists y ∈ β with the fiber size bounded above by n, given a total bound on the sum and a finite domain.
Русский
Существует y ∈ β такое, что размер фибера над y не превышает n, при конечном домене и суммарном ограничении.
LaTeX
$$$\\exists y \\in t,\\; \\#\\{x \\in s \\mid f(x) = y\\} \\le n$$$
Lean4
/-- 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. -/
theorem exists_lt_card_fiber_of_mul_lt_card (hn : card β * n < card α) : ∃ y : β, n < #{x | f x = y} :=
exists_lt_card_fiber_of_nsmul_lt_card _ hn
