English
A variant of pigeonhole: under bounds on each fiber and a global bound, there exists a fiber with target membership and a bound satisfaction.
Русский
Лемма о левой сумме, вариант теоремы о кластерах: существует волокно с требуемым свойством.
LaTeX
$$$\\exists y ∈ t, \\text{lt bound on fiber}$$$
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 greater than `n • b`, they are sorted into some
pigeonholes, and for all but `n` pigeonholes the total weight of the pigeons there is nonpositive,
then for at least one of these `n` pigeonholes, the total weight of the pigeons in this pigeonhole
is greater than `b`. -/
theorem exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum (ht : ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0)
(hb : #t • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x :=
exists_lt_of_sum_lt <|
calc
∑ _y ∈ t, b < ∑ x ∈ s, w x := by simpa
_ ≤ ∑ y ∈ t, ∑ x ∈ s with f x = y, w x := sum_le_sum_fiberwise_of_sum_fiber_nonpos ht
