Skip to content

Erdős problem 590

Let αα be the infinite ordinal ωω\omega^{\omega}. It was proved by Chang [Ch72] that any red/blue colouring of the edges of KαK_α there is either a red KαK_α or a blue K3K_3.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

590.lean

Retained formal statement2 of 4

Let m be a finite cardinal <ω< \omega. Let αα be the infinite ordinal ωω\omega^{\omega}. It was proved by Milnor that any red/blue colouring of the edges of KαK_α there is either a red KαK_α or a blue K3K_3. A shorter proof was found by Larson [La73]

FormalConjectures/ErdosProblems/590.leanErdos590.erdos_590.variants.finite_cardinal1 lineExact file
∀ (m : ℕ), OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0) (Ordinal.omega0 ^ Ordinal.omega0) ↑m
SolvedStatement only, no proof