English
There exists y ∈ t such that nsmul bounds imply a fiber bound via multiplication.
Русский
Существует y ∈ t, для которого умножение даёт требуемое ограничение по фибру.
LaTeX
$$$\\exists y ∈ t, n < #({x ∈ s | f x = y})$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.
("The maximum is at least the mean" specialized to integers.)
More formally, given a function between finite sets `s` and `t` and a natural number `n` such that
`#t * n < #s`, there exists `y ∈ t` such that its preimage in `s` has more than `n`
elements. -/
theorem exists_lt_card_fiber_of_mul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (hn : #t * n < #s) :
∃ y ∈ t, n < #({x ∈ s | f x = y}) :=
exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to hf hn
