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
Monotonicity: If G is a countable union of triangle-free graphs and H ≤ G (i.e., H is a subgraph of G), then H is also a countable union of triangle-free graphs.
Proof: If G = ⨆ i, G_i with each G_i triangle-free, then H = ⨆ i, H ⊓ G_i. Each H ⊓ G_i is triangle-free because it is a subgraph of G_i.
∀ {V : Type u_1} {G H : SimpleGraph V}, H ≤ G → Erdos595.IsCountableUnionOfTriangleFree G → Erdos595.IsCountableUnionOfTriangleFree HTextbookStatement only, no proof