English
If hf ensures the image of s lies in t, t is nonempty, and #t · n ≤ #s, then there exists y ∈ t with n ≤ #{x ∈ s | f(x) = y}.
Русский
Если hf гарантирует, что образ s лежит в t, t непусто и #t·n ≤ #s, то существует y ∈ t такое, что n ≤ #{x ∈ s | f(x) = y}.
LaTeX
$$$\\exists y \\in t,\\; n \\le \\#\\{x \\in s \\mid f(x) = y\\}$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
finite sets `s` and `t`, and a number `b` such that `#s ≤ #t • b`, there exists `y ∈ t` such
that its preimage in `s` has no more than `b` elements.
See also `Finset.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement. -/
theorem exists_card_fiber_le_of_card_le_nsmul (ht : t.Nonempty) (hb : #s ≤ #t • b) :
∃ y ∈ t, #({x ∈ s | f x = y}) ≤ b := by
simp_rw [cast_card] at hb ⊢
refine exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb
