Erdős problem 595
Erdős Problem 595 (250): Is there an infinite graph G which contains no and is not the union of countably many triangle-free graphs?
Sources
FormalConjectures/ErdosProblems/
595.lean
Retained formal statement
Reformulation via edge colourings: A graph G is a countable union of triangle-free graphs if and only if there is a colouring of the edges of G by ℕ such that no monochromatic triangle exists.
More precisely: IsCountableUnionOfTriangleFree G is equivalent to the existence of a map c : G.edgeSet → ℕ such that for each n : ℕ, the subgraph of edges coloured n is triangle-free.
∀ {V : Type u_1} (G : SimpleGraph V), Erdos595.IsCountableUnionOfTriangleFree G ↔ ∃ c, ∀ (n : ℕ), (SimpleGraph.fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3TestStatement only, no proof