English
Let s and t be finite, f: s → t with maps-to condition; if the product |t| · n is at most |s|, then there exists y ∈ t with n ≤ |{x ∈ s | f(x) = y}|.
Русский
Пусть s, t - конечные; f: s → 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 between
finite sets `s` and `t` and a natural number `b` such that `#t * n ≤ #s`, there exists
`y ∈ t` such that its preimage in `s` has at least `n` elements. See also
`Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to` for a stronger statement. -/
theorem exists_le_card_fiber_of_mul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hn : #t * n ≤ #s) :
∃ y ∈ t, n ≤ #({x ∈ s | f x = y}) :=
exists_le_card_fiber_of_nsmul_le_card_of_maps_to hf ht hn
