Skip to content

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

Open selected source

FormalConjectures/ErdosProblems/

593.lean

Retained formal statement10 of 10

Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal >ℵ0> \aleph_0 must have an uncountable vertex set.

Proof: If V is countable, there exists an injection φ : V → ℕ. Using distinct natural numbers as colors gives a proper coloring, so χ(H)≤#N=ℵ0\chi(H) \leq \#\mathbb{N} = \aleph_0, contradicting χ(H)>ℵ0\chi(H) > \aleph_0.

FormalConjectures/ErdosProblems/593.leanErdos593.erdos_593.variants.uncountable_vertices_if_large_chromatic1 lineExact file
∀ {V : Type} (H : ThreeUniformHypergraph V), Cardinal.aleph0 < H.chromaticCardinal → ¬Countable V
TextbookStatement only, no proof