English
A strong version: given a finite mapping, there exists a hole with fiber strictly larger than a bound when the total weight exceeds a bound.
Русский
Усиленная форма: существует дыра, для которой размер фибера больше порога, если суммарный вес превышает порог.
LaTeX
$$∃ y ∈ t, b < #{x ∈ s | f(x) = y}$$
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 α ≤ card β * n`, there exists an
element `y : β` such that its preimage has at most `n` elements. See also
`Fintype.exists_card_fiber_lt_of_card_lt_mul` for a stronger statement. -/
theorem exists_card_fiber_le_of_card_le_mul [Nonempty β] (hn : card α ≤ card β * n) : ∃ y : β, #{x | f x = y} ≤ n :=
exists_card_fiber_le_of_card_le_nsmul _ hn
