Skip to content

Erdős problem 918

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

Browse retained paths and inspect the exact material available for this Problem.

9 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

918.lean

Retained formal statement9 of 9

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.

FormalConjectures/ErdosProblems/918.leanErdos918.erdos_918.variants.erdos_hajnal7 linesExact file
∀ (k : ℕ),  0 < kV G,      Cardinal.mk V = Cardinal.alephk        G.chromaticCardinal = Cardinal.aleph 1 ∧          ∀ (W : Set V),            Cardinal.mkW < Cardinal.alephk → (SimpleGraph.induce W G).chromaticCardinalCardinal.aleph0
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page