English
Let s ⊆ A and t ⊆ B be finite, f: A → B with hf saying f(a) ∈ t for all a ∈ s. If t is nonempty and |t| · b ≤ |s|, then there exists y ∈ t with b ≤ |{x ∈ s | f(x) = y}|.
Русский
Пусть s ⊆ A, t ⊆ B - конечные; f: A → B так, что для всех a ∈ s выполняется f(a) ∈ t; если t непусто и |t|·b ≤ |s|, то существует y ∈ t такое, что b ≤ |{x ∈ s | f(x) = y}|.
LaTeX
$$$\\exists y \\in t,\\; b \\le \\#\\{x \\in s \\mid f(x) = y\\}$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
finite sets `s` and `t` and a number `b` such that `#t • b ≤ #s`, there exists `y ∈ t` such
that its preimage in `s` has at least `b` elements.
See also `Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` for a stronger statement. -/
theorem exists_le_card_fiber_of_nsmul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : #t • b ≤ #s) :
∃ y ∈ t, b ≤ #({x ∈ s | f x = y}) := by
simp_rw [cast_card] at hb ⊢
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb
