Theorems · Theorem · combinatorics

Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul

∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ y ∉ t, 0 ≤ ∑ x ∈ s with f x = y, w x) →
    t.Nonempty → ∑ x ∈ s, w x ≤ t.card • b → ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b

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.

Defined in

Mathlib.Combinatorics.Pigeonhole

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddCommMonoidLinearOrderIsOrderedCancelAddMonoid