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
Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75]): For the 2-uniform (graph) case, a graph of chromatic cardinal must contain all finite bipartite graphs. Specifically, for every finite bipartite graph F and every graph G with chromatic cardinal , there is a graph embedding from F into G.
This uses Nonempty (F ↪g G) (graph embedding), aligned with the injective vertex map used in the hypergraph Appears definition.
True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)