English
If α is infinite and β finite, then there exists y ∈ β such that f^{-1}({y}) is infinite.
Русский
Если α бесконечно и β конечно, тогда существует y ∈ β такое, что f^{-1}({y}) бесконечно.
LaTeX
$$$\\exists y: \\beta, Infinite\\left(f^{-1}({y})\\right).$$$
Lean4
/-- The strong pigeonhole principle for infinitely many pigeons in
finitely many pigeonholes. If there are infinitely many pigeons in
finitely many pigeonholes, then there is a pigeonhole with infinitely
many pigeons.
See also: `Finite.exists_ne_map_eq_of_infinite`
-/
theorem exists_infinite_fiber [Infinite α] [Finite β] (f : α → β) : ∃ y : β, Infinite (f ⁻¹' { y }) := by
classical
by_contra! hf
cases nonempty_fintype β
let key : Fintype α :=
{ elems := univ.biUnion fun y : β => (f ⁻¹' { y }).toFinset
complete := by simp }
exact key.false
