English
In the sum-form with finite domains, there exists a hole y with the sum of weights in its fibre bounded by b.
Русский
В суммарной форме существует дыра y, для которой сумма весов в её фибере не превосходит b.
LaTeX
$$$\\exists y \\in \\mathrm{univ},\\; \\sum_{x \\in \\mathrm{univ} \\;:\\; f(x)=y} w(x) \\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 β • b ≤ card α`, there exists an
element `y : β` such that its preimage has at least `b` elements.
See also `Fintype.exists_lt_card_fiber_of_nsmul_lt_card` for a stronger statement. -/
theorem exists_le_card_fiber_of_nsmul_le_card [Nonempty β] (hb : card β • b ≤ card α) : ∃ y : β, b ≤ #{x | f x = y} :=
let ⟨y, _, h⟩ := exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun _ _ => mem_univ _) univ_nonempty hb
⟨y, h⟩
