Erdős problem 593
Which finite triple systems occur in every triple system of uncountable chromatic number? The claimed characterization: exactly those that, after removing isolated vertices, are linear, have every hyperedge-node of their Levi graph meeting a bridge, and have every Berge cycle even.
Sources
FormalConjectures/ErdosProblems/
593.lean
Retained formal statement
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, implies H has at least one hyperedge.
∀ {V : Type} (H : ThreeUniformHypergraph V), Cardinal.aleph0 < H.chromaticCardinal → H.edges.NonemptyTextbookStatement only, no proof