Ramsey theorem for infinite graphs

This result really should be in Mathlib, but currently it is not. We do expect the Ramsey theorem for infinite hypergraphs to appear in Mathlib eventually and this result to be derived as a corollary of the more general result.

theorem Cslib.infinite_pigeonhole_principle {X : Type u_1} {Y : Type u_2} [Finite Y] (f : X → Y) {s : Set X} (h_inf : s.Infinite) : ∃ (y : Y) (t : Set X), t.Infinite ∧ t ⊆ s ∧ ∀ x ∈ t, f x = y

An infinite pigeonhole principle.

theorem Cslib.infinite_graph_ramsey {Vertex : Type u_1} {Color : Type u_2} [Finite Color] (color : Finset Vertex → Color) [Infinite Vertex] : ∃ (c : Color) (s : Set Vertex), s.Infinite ∧ ∀ (e : Finset Vertex), e.card = 2 → ↑e ⊆ s → color e = c

If the edges of an infinite complete graph is assigned a finite number of colors, then there must exist a color c and an infinite set s of vertices such that the edge beteen any two vertices of s is assigned the same color c.