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

Monotonicity of the obligatory property: If F₁ appears in F₂ and F₂ is obligatory, then F₁ is also obligatory.

Proof: For any H with $\chi(H) > \aleph_0$ , since F₂ is obligatory, F₂ appears in H via some injection φ₂. Since F₁ appears in F₂ via φ₁, the composition φ₂ ∘ φ₁ witnesses that F₁ appears in H.

FormalConjectures/ErdosProblems/593.leanErdos593.erdos_593.variants.obligatory_monotone2 linesExact file

1∀ {W₁ W₂ : Type} [inst : Fintype W₁] [inst_1 : Fintype W₂] [inst_2 : DecidableEq W₂] {F₁ : ThreeUniformHypergraph W₁}2  {F₂ : ThreeUniformHypergraph W₂}, F₁.Appears F₂ → IsObligatory F₂ → IsObligatory F₁

TextbookStatement only, no proof