Skip to content

Erdős problem 1175

Start work

Let κ\kappa be an uncountable cardinal. Must there exist a cardinal λ\lambda such that every graph with chromatic number λ\lambda contains a triangle-free subgraph with chromatic number κ\kappa?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1175.lean

Retained formal statement5 of 5

Threshold reformulation variant. Replaces chromaticCardinal = λ in the hypothesis of erdos_1175 with λ ≤ chromaticCardinal (a graph of chromatic number ≥ λ has a triangle-free subgraph of chromatic number κ). This is a strengthening of erdos_1175 (see erdos_1175.test.threshold_implies_exact).

FormalConjectures/ErdosProblems/1175.leanErdos1175.erdos_1175.variants.threshold_formulation6 linesExact file
True ↔  ∀ (κ : Cardinal.{u_1}),    Cardinal.aleph0 < κ →      ∃ μ,        ∀ (V : Type u_1) (G : SimpleGraph V),          μ ≤ G.chromaticCardinal → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ
OpenStatement only, no proof