def RamseyGraphProp (N s t : ℕ) : Prop

Equations

• RamseyGraphProp N s t = ∀ (G : SimpleGraph (Fin N)) [DecidableRel G.Adj], (∃ (S : Finset (Fin N)), G.IsNClique s S) ∨ ∃ (T : Finset (Fin N)), G.IsNIndepSet t T

theorem RamseyGraphMonotone {N s t : ℕ} : RamseyGraphProp N s t → ∀ {M : ℕ}, N ≤ M → RamseyGraphProp M s t

theorem RamseyGraphPropSymm (N s t : ℕ) : RamseyGraphProp N s t ↔ RamseyGraphProp N t s

noncomputable def GraphRamsey (s t : ℕ) : ℕ

Equations

• GraphRamsey s t = sInf {N : ℕ | RamseyGraphProp N s t}

theorem GraphRamsey2 (k : ℕ) : GraphRamsey 2 k.succ = k.succ

theorem RamseyGraph1Prop (N k : ℕ) : RamseyGraphProp N.succ 1 k

theorem RamseyGraph1 (k : ℕ) : GraphRamsey 1 k.succ = 1

theorem R34 : ¬RamseyGraphProp 8 3 4

theorem R35 : ¬RamseyGraphProp 13 3 5

theorem R44' : ¬RamseyGraphProp 17 4 4

theorem R36 : RamseyGraphProp 18 3 6