Catalog/Sparsity/MulticolorRamsey/Contract.lean

1	import Mathlib.Combinatorics.SimpleGraph.Clique
2
3	namespace Catalog.Sparsity.MulticolorRamsey
4
5	/-- Multicolor Ramsey theorem: for any list of natural numbers
6	`sizes = [n₁, …, nₖ]`, there exists `N` such that every `k`-coloring of
7	edges of a complete graph on at least `N` vertices yields a monochromatic
8	clique of size `nᵢ` in color `i`, for some `i`. (Theorem 3.8) -/
9	axiom multicolorRamsey (sizes : List ℕ) (hk : sizes ≠ []) :
10	∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V],
11	N ≤ Fintype.card V →
12	∀ (c : Sym2 V → Fin sizes.length),
13	∃ (i : Fin sizes.length) (S : Finset V),
14	sizes.get i ≤ S.card ∧
15	(↑S : Set V).Pairwise (fun u v => c s(u, v) = i)
16
17	end Catalog.Sparsity.MulticolorRamsey
18