Infinite pigeonhole on ℕ

Set-valued restatement of Finite.exists_infinite_fiber for sequences indexed by ℕ. Both the direct proof of the infinite Ramsey theorem and the Nash-Williams development iterate this, so it is kept here rather than in either of them.

Main results

• exists_infinite_fiber_nat: a finitely-valued sequence f : ℕ → κ is constant on an infinite set.

Upstream target: Mathlib/Data/Fintype/Pigeonhole.lean.

theorem exists_infinite_fiber_nat {κ : Type u_1} [Finite κ] (f : ℕ → κ) : ∃ (k : κ), {n : ℕ | f n = k}.Infinite

Infinite pigeonhole. A sequence f : ℕ → κ with κ finite takes some value k on an infinite set of indices.