English
For finite domains with weights w(x) assigning to each x, if the total weight across all y in β is less than the total weight, then there exists some y with the total weight assigned to x mapping to y exceeding a threshold.
Русский
Для конечных доменов со взвешиваниями w(x) по элементам, если суммарный вес по всем направлениям меньше общего веса, найдется направление с весом выше порога.
LaTeX
$$$\\exists y, \\sum_{x: f(x)=y} w(x) > b$ (варианты внутри доказательства различаются по знаку и нечеткости условий)$$
Lean4
/-- The pigeonhole principle for finitely many pigeons of different weights, strict inequality
version: there is a pigeonhole with the total weight of pigeons in it less than `b` provided that
the total number of pigeonholes times `b` is greater than the total weight of all pigeons. -/
theorem exists_sum_fiber_lt_of_sum_lt_nsmul (hb : ∑ x, w x < card β • b) : ∃ y, ∑ x with f x = y, w x < b :=
exists_lt_sum_fiber_of_nsmul_lt_sum (M := Mᵒᵈ) _ hb
