Erdős problem 1176

Let $G$ be a graph with chromatic number $\aleph_1$ . Is it true that there is a colouring of the edges with $\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

1176.lean

Retained formal statement1 of 1

Let $G$ be a graph with chromatic number $\aleph_1$ . Is it true that there is a colouring of the edges with $\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?

A problem of Erdős, Galvin, and Hajnal. The consistency of this was proved by Hajnal and Komjáth.

FormalConjectures/ErdosProblems/1176.leanErdos1176.erdos_117611 linesExact file

1True ↔2  ∀ {V : Type u_1} (G : SimpleGraph V),3    G.chromaticCardinal = Cardinal.aleph 1 →4      ∃ EColor,5        ∃ (_ : Cardinal.mk EColor = Cardinal.aleph 1),6          ∃ c_edge,7            ∀ (VColor : Type),8              Cardinal.mk VColor ≤ Cardinal.aleph 0 →9                ∀ (c_vert : V → VColor),10                  ∃ vc,11                    ∀ (ec : EColor), ∃ u v, ∃ (h : G.Adj u v), c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec

OpenStatement only, no proof