Erdős Problem 108 #
Reference: erdosproblems.com/108
theorem
Erdos108.erdos_108
{V : Type u}
:
(∀ r ≥ 4,
∀ k ≥ 2,
∃ (f : ℕ),
∀ (G : SimpleGraph V),
G.chromaticNumber ≤ ↑f → ∃ (H : G.Subgraph), H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ k) ↔ sorry
For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?