English
Let s and t be finite with t nonempty and hb: #s ≤ #t · b. Then there exists y ∈ t with #{x ∈ s | f(x) = y} ≤ b.
Русский
Пусть t непусто и #s ≤ #t · b. Тогда существует y ∈ t такое, что #{x ∈ s | f(x) = y} ≤ b.
LaTeX
$$$\\exists y \\in t,\\; \\#\\{x \\in s \\mid f(x) = y\\} \\le b$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
finite sets `s` in its domain, a finite set `t` in its codomain, and a natural number `n` such that
`#s ≤ #t * n`, there exists `y ∈ t` such that its preimage in `s` has no more than `n`
elements. See also `Finset.exists_card_fiber_lt_of_card_lt_mul` for a stronger statement. -/
theorem exists_card_fiber_le_of_card_le_mul (ht : t.Nonempty) (hn : #s ≤ #t * n) : ∃ y ∈ t, #({x ∈ s | f x = y}) ≤ n :=
exists_card_fiber_le_of_card_le_nsmul ht hn
