English
For finite s,t and f with t mapped into by s, the existence of a y ∈ t with b ≤ |fiber| is guaranteed when |t|·b ≤ |s|.
Русский
Для конечных s,t и отображения f между ними, если |t|·b ≤ |s|, то существует y ∈ t с b ≤ размер фибера.
LaTeX
$$$\\exists y \\in t,\\; b \\le \\#\\{x \\in s \\mid f(x) = y\\}$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality
version: there is a pigeonhole with the total weight of pigeons in it greater than or equal to `b`
provided that the total number of pigeonholes times `b` is less than or equal to the total weight of
all pigeons. -/
theorem exists_le_sum_fiber_of_nsmul_le_sum [Nonempty β] (hb : card β • b ≤ ∑ x, w x) :
∃ y, b ≤ ∑ x with f x = y, w x :=
let ⟨y, _, hy⟩ := exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum (fun _ _ => mem_univ _) univ_nonempty hb
⟨y, hy⟩
