English
There exists a nonempty t with fibre bound in a non-strict inequality: if t is nonempty and the sum bound holds, then a fibre is small.
Русский
Существует непустое t, у которого фибер ограничен нестрогим образом: если сумма ограничена, то найдётся маленький фибер.
LaTeX
$$$\\exists y \\in t,\\; \\#\\{x \\in s \\mid f(x)=y\\} \\le b$$$
Lean4
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function `f`
between finite types `α` and `β` and a number `b` such that `card α ≤ card β • b`, there exists an
element `y : β` such that its preimage has at most `b` elements.
See also `Fintype.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement. -/
theorem exists_card_fiber_le_of_card_le_nsmul [Nonempty β] (hb : ↑(card α) ≤ card β • b) :
∃ y : β, #{x | f x = y} ≤ b :=
let ⟨y, _, h⟩ := Finset.exists_card_fiber_le_of_card_le_nsmul univ_nonempty hb
⟨y, h⟩
