Erdős problem 593

Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.

Sources

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

593.lean

Retained formal statement6 of 10

No hyperedges implies chromatic cardinal ≤ 1: A 3-uniform hypergraph with no edges can be properly colored with a single color, so its chromatic cardinal is at most 1. In particular, $\chi(H) > \aleph_0$ implies H has at least one hyperedge.

FormalConjectures/ErdosProblems/593.leanErdos593.erdos_593.variants.nonempty_edges_if_large_chromatic1 lineExact file

1∀ {V : Type} (H : ThreeUniformHypergraph V), Cardinal.aleph0 < H.chromaticCardinal → H.edges.Nonempty

TextbookStatement only, no proof