Erdős problem 617
Let . If the edges of are -coloured then there exist vertices with at least one colour missing on the edges of the induced .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/617.lean∀ r ≥ 3, ∀ {V : Type} [inst : Fintype V] [DecidableEq V], Fintype.card V = r ^ 2 + 1 → ∀ (coloring : Sym2 V → Fin r), ∃ S k, S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ kOpenStatement only, no proof