Erdős problem 590
Let be the infinite ordinal . It was proved by Chang [Ch72] that any red/blue colouring of the edges of there is either a red or a blue .
Sources
FormalConjectures/ErdosProblems/
590.lean
Retained formal statement
Specker [Sp57] proved that when for then it is not the case that any red/blue colouring of the edges of there is either a red or a blue .
∀ {n : ℕ}, 3 ≤ n → ¬OrdinalCardinalRamsey (Ordinal.omega0 ^ n) (Ordinal.omega0 ^ n) 3SolvedStatement only, no proof