Catalog/Sparsity/Ramsey/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 2 | |
| 3 | namespace Catalog.Sparsity.Ramsey |
| 4 | |
| 5 | /-- Ramsey's theorem (two colors): for any `a b : ℕ` there exists `N` such that |
| 6 | every graph on at least `N` vertices either contains a clique of size `a` or |
| 7 | an independent set of size `b`. (Theorem 3.7) -/ |
| 8 | axiom ramsey (a b : ℕ) : ∃ N : ℕ, |
| 9 | ∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V) |
| 10 | [DecidableRel G.Adj], |
| 11 | N ≤ Fintype.card V → ¬G.CliqueFree a ∨ ¬Gᶜ.CliqueFree b |
| 12 | |
| 13 | end Catalog.Sparsity.Ramsey |
| 14 |