def Ramsey.graphAtColor {N k : ℕ} (G : SimpleGraph (Fin N)) (f : Sym2 (Fin N) → Fin k) (i : Fin k) : SimpleGraph (Fin N)

Equations

• Ramsey.graphAtColor G f i = { Adj := fun (u v : Fin N) => G.Adj u v ∧ f s(u, v) = i, symm := ⋯, loopless := ⋯ }

instance Ramsey.instDecidableRelFinAdjGraphAtColor {N k : ℕ} (G : SimpleGraph (Fin N)) [DecidableRel G.Adj] (f : Sym2 (Fin N) → Fin k) (i : Fin k) : DecidableRel (graphAtColor G f i).Adj

Equations

• One or more equations did not get rendered due to their size.

def Ramsey.RamseyProp {k : ℕ} (N : ℕ) (s : List.Vector ℕ k.succ) : Prop

Equations

• Ramsey.RamseyProp N s = ∀ (f : Sym2 (Fin N) → Fin k.succ), ∃ (S : Finset (Fin N)) (i : Fin k.succ), (Ramsey.graphAtColor ⊤ f i).IsNClique (s.get i) S

instance Ramsey.instDecidablePredNatMemSetSetOfRamseyProp (k : ℕ) (s : List.Vector ℕ k.succ) : DecidablePred (Membership.mem {N : ℕ | RamseyProp N s})

Equations

• Ramsey.instDecidablePredNatMemSetSetOfRamseyProp k s N = id inferInstance

theorem Ramsey.RamseyProp0 {k : ℕ} {s : List.Vector ℕ k.succ} : RamseyProp 0 s → ∃ (i : Fin k.succ), s.get i = 0

theorem Ramsey.RamseyMonotone {N k : ℕ} {s : List.Vector ℕ k.succ} : RamseyProp N s → ∀ {M : ℕ}, N ≤ M → RamseyProp M s

def Ramsey.monochromaticVicinity {α : Type} [Fintype α] {c : ℕ} (g : SimpleGraph α) [DecidableRel g.Adj] (v : α) (f : Sym2 α → Fin c) (i : Fin c) : Finset α

Equations

• Ramsey.monochromaticVicinity g v f i = {x ∈ g.neighborFinset v | f s(v, x) = i}

theorem Ramsey.monochromaticVicinity_Ramsey {N c : ℕ} {v : Fin N} {f : Sym2 (Fin N) → Fin c.succ} {i : Fin c.succ} {s : List.Vector ℕ c.succ} : RamseyProp (monochromaticVicinity ⊤ v f i).card s → (∃ (S : Finset (Fin N)), (graphAtColor ⊤ f i).IsNClique (s.get i).succ S) ∨ ∃ (i' : Fin c.succ) (S : Finset (Fin N)), i' ≠ i ∧ (graphAtColor ⊤ f i').IsNClique (s.get i') S