Skip to content

Erdős problem 918

Start work

A question of Erdős and Hajnal [ErHa68b], who proved that for every finite kk there is a graph with chromatic number ℵ1\aleph_1 and ℵk\aleph_k vertices where each subgraph on less than ℵk\aleph_k vertices has chromatic number ≤ℵ0\leq \aleph_0.

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

918.lean

Retained formal statement7 of 9

In [ErHa69] the questions are stated with =ℵ0= \aleph_0 rather than ≤ℵ0\leq\aleph_0. This is a likely typo since it can be shown that no such graph exists in this case.

This is the first question with induced subgraphs.

FormalConjectures/ErdosProblems/918.leanErdos918.erdos_918.variants.eq_aleph_0.parts.i4 linesExact file
¬∃ V G,    Cardinal.mk V = Cardinal.aleph 2 ∧      G.chromaticCardinal = Cardinal.aleph 2 ∧        ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal = Cardinal.aleph0
TextbookStatement only, no proof