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?

AMS 3 5 · open (literature)

theorem erdos_1176 :
    answer(sorry) ↔ ∀ {V : Type*} (G : SimpleGraph V), G.chromaticCardinal = aleph 1 →
      ∃ (EColor : Type) (_ : mk EColor = aleph 1) (c_edge : G.edgeSet → EColor),
        ∀ (VColor : Type) (_ : mk VColor ≤ aleph 0) (c_vert : V → VColor),
          ∃ (vc : VColor),
            ∀ (ec : EColor), ∃ (u v : V) (h : G.Adj u v),
              c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec