Erdős problem 593 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

12 retained statements2415f78e850a

Open selected source

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

Sources

Search problems.science