English
In a finite setting there is a dual inequality version: if total weighted sum in an opposite sense exceeds a bound, a fibre exceeds a bound in the opposite direction.
Русский
В конечной постановке существует дуальная неравенство: если суммарный вес превышает предел, то один фибер превышает предел в противоположном направлении.
LaTeX
$$$\\exists y \\in t,\\; \\sum_{x \\in s \\mid f(x)=y} w(x) \\ge b$$$
Lean4
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function `f`
between finite types `α` and `β` and a number `n` such that `card β * n ≤ card α`, there exists an
element `y : β` such that its preimage has at least `n` elements. See also
`Fintype.exists_lt_card_fiber_of_mul_lt_card` for a stronger statement. -/
theorem exists_le_card_fiber_of_mul_le_card [Nonempty β] (hn : card β * n ≤ card α) : ∃ y : β, n ≤ #{x | f x = y} :=
exists_le_card_fiber_of_nsmul_le_card _ hn
