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
The complete graph `⊤` on `ℕ` is a countable union of triangle-free graphs: we decompose it into the family of star graphs {H_m}_{m : ℕ}, where H_m is the graph with edges {m, n} for all n ≠ m. Each star is triangle-free (any two non-center vertices share no edge within the star), and their union covers all edges of ⊤.
Proof sketch (star triangle-free): If {a, b, c} were a triangle in H_m, then each of the three edges {a, b}, {a, c}, {b, c} would pass through m. In particular, from {a, b} we get a = m or b = m; from {b, c} we get b = m or c = m. Case analysis shows that two vertices must equal m, contradicting the triangle having three distinct vertices.
Erdos595.IsCountableUnionOfTriangleFree ⊤