English
There exists a y with fibre size bound in the sum-form: if the total unweighted sum across all x is less than the total capacity, then some fibre is small.
Русский
Существует y с ограничением размера фибера по сумме: если общая сумма меньше общей вместимости, то некоторый фибер мал.
LaTeX
$$$\\exists y \\in t,\\; \\Big( \\sum_{x \\in s \\mid f(x)=y} 1 \\Big) \\le b$$$
Lean4
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.
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` between finite types `α` and `β` and a number `n` such that
`card α < card β * n`, there exists an element `y : β` such that its preimage has less than `n`
elements. -/
theorem exists_card_fiber_lt_of_card_lt_mul (hn : card α < card β * n) : ∃ y : β, #{x | f x = y} < n :=
exists_card_fiber_lt_of_card_lt_nsmul _ hn
