erdos_617.variant.r_eq_3

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

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

Recent Submissions

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