English
If weights over a finite set map into a target with a nonempty target, the total weight exceeds the sum of per-target bounds, then there exists a target whose accumulated weight exceeds its bound when summing over fibers.
Русский
Если суммарный вес перегружает одно из целевых значений, найдётся целевой элемент с превосходящим весом по фибрам.
LaTeX
$$$\\exists y ∈ t, b < \\sum_{x\\in s: f(x)=y} w(x)$ under the given decomposition$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is less than `n • b`, and they are sorted into `n`
pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is less
than `b`. -/
theorem exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul (hf : ∀ a ∈ s, f a ∈ t) (hb : ∑ x ∈ s, w x < #t • b) :
∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b :=
exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum (M := Mᵒᵈ) hf hb
