Skip to content

Erdős problem 594

Start work

Erdős Problem 594 (Erdős–Hajnal [ErHa66], [Er69b]):

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

594.lean

Retained formal statement3 of 3

The earlier result of Erdős and Hajnal [ErHa66]: every graph with chromatic number ≥ℵ2\geq \aleph_2 contains all sufficiently large odd cycles.

Chromatic number ≥ℵ2\geq \aleph_2 is encoded as the nonexistence of a proper colouring with any set of at most ℵ1\aleph_1 colours.

FormalConjectures/ErdosProblems/594.leanErdos594.erdos_594.variants.erdos_hajnal3 linesExact file
∀ (V : Type) (G : SimpleGraph V),  (∀ (α : Type), Cardinal.mk α ≤ Cardinal.aleph 1 → IsEmpty (G.Coloring α)) →    ∃ N, ∀ (k : ℕ), N ≤ k → ∃ v w, w.IsCycle ∧ w.length = 2 * k + 1
SolvedStatement only, no proof