Erdős problem 740
Let be an infinite cardinal and be a graph with chromatic number . Let . Must contain a subgraph of chromatic number which does not contain any odd cycle of length ?
Sources
FormalConjectures/ErdosProblems/
740.lean
Retained formal statement
Let be an infinite cardinal and be a graph with chromatic number . Let . Must contain a subgraph of chromatic number which does not contain any odd cycle of length ?
True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe rOpenStatement only, no proof