English
If a finite set under a mapping to a finite target has a bound relation, there exists a fiber with the bound property.
Русский
Пусть отображение из конечного множества в конечную мишень соблюдает ограничительную связь; существует фибр с требуемым свойством.
LaTeX
$$$\\exists \\cdot ∈ \\cdot$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is less than or equal to `n • b`, they are
sorted into some pigeonholes, and for all but `n > 0` pigeonholes the total weight of the pigeons
there is nonnegative, then for at least one of these `n` pigeonholes, the total weight of the
pigeons in this pigeonhole is less than or equal to `b`. -/
theorem exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul (hf : ∀ y ∉ t, (0 : M) ≤ ∑ x ∈ s with f x = y, w x)
(ht : t.Nonempty) (hb : ∑ x ∈ s, w x ≤ #t • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b :=
exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum (M := Mᵒᵈ) hf ht hb
