English
Let s and t be finite sets and f: s → t. If the total number of elements in s is strictly less than b times the number of elements in t, then there exists a hole y in t such that the number of elements of s that map to y is less than b.
Русский
Пусть s и t - конечные множества и f: s → t. Если |s| < b · |t|, то существует некоторый ящик y в t, в который попадает меньше чем b элементов из s.
LaTeX
$$$\\exists y \\in t, \\#\\{x \\in s \\mid f(x) = y\\} < b$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. -/
theorem exists_card_fiber_lt_of_card_lt_nsmul (ht : #s < #t • b) : ∃ y ∈ t, #({x ∈ s | f x = y}) < b :=
by
simp_rw [cast_card] at ht ⊢
exact exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht
