Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem
Submitter: Kim Morrison.
Notes: States finite Ramsey existence for red/blue edge colourings of complete graphs, encoded by a graph and its complement.
Source: Classical theorem in Ramsey theory.
Informal solution: Show that for every r and s there is an n such that every graph on n vertices contains either a clique of size r or an independent set of size s.
theorem declaration uses `sorry`finite_graph_ramsey_theorem :
∀ r s : ℕ, 2 ≤ r → 2 ≤ s → ∃ n : ℕ, ∀ G : SimpleGraph (Fin n), ¬ G.CliqueFree r ∨ ¬ Gᶜ.CliqueFree s := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s
All goals completed! 🐙