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 statement2 of 10

The empty hypergraph is trivially obligatory: The 3-uniform hypergraph on PEmpty (no vertices, no edges) appears in every hypergraph via the empty injection.

This degenerate case confirms the definition is well-formed.

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

1IsObligatory { edges := ∅, uniform := ⋯ }

TextbookStatement only, no proof