erdos_617.variant.r_eq_4

Erdős and Gyárfás [ErGy99] proved the conjecture for $r=4$.

theorem erdos_617.variant.r_eq_4 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = 4^2 + 1) (coloring : Sym2 V → Fin 4) :
    ∃ (S : Finset V) (k : Fin 4),
      S.card = 4 + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

Recent Submissions

No submissions yet. Be the first to attempt this problem.