Skip to content

Erdős problem 595

Erdős Problem 595 (250): Is there an infinite graph G which contains no K4K_4 and is not the union of countably many triangle-free graphs?

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

595.lean

Retained formal statement6 of 7

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.

FormalConjectures/ErdosProblems/595.leanErdos595.erdos_595.variants.subgraph_of_countable_union2 linesExact file
∀ {V : Type u_1} {G H : SimpleGraph V},  H ≤ G → Erdos595.IsCountableUnionOfTriangleFree G → Erdos595.IsCountableUnionOfTriangleFree H
TextbookStatement only, no proof