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 statement3 of 5

The threshold variant threshold_formulation is stronger than the exact-equality form erdos_1175: if every graph with chromaticCardinal ≥ μ has the desired triangle-free subgraph, then in particular every graph with chromaticCardinal = μ does too.

FormalConjectures/ErdosProblems/1175.leanErdos1175.erdos_1175.test.threshold_implies_exact10 linesExact file
(∀ (κ : Cardinal.{0}),    Cardinal.aleph0 < κ →      ∃ μ,        ∀ (V : Type) (G : SimpleGraph V),          μ ≤ G.chromaticCardinal → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ) →  ∀ (κ : Cardinal.{0}),    Cardinal.aleph0 < κ →      ∃ μ,        ∀ (V : Type) (G : SimpleGraph V),          G.chromaticCardinal = μ → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ
TestStatement only, no proof