Erdős problem 740

Let $\mathfrak{m}$ be an infinite cardinal and $G$ be a graph with chromatic number $\mathfrak{m}$ . Let $r\geq 1$ . Must $G$ contain a subgraph of chromatic number $\mathfrak{m}$ which does not contain any odd cycle of length $\leq r$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

740.lean

Retained formal statement1 of 1

Let $\mathfrak{m}$ be an infinite cardinal and $G$ be a graph with chromatic number $\mathfrak{m}$ . Let $r\geq 1$ . Must $G$ contain a subgraph of chromatic number $\mathfrak{m}$ which does not contain any odd cycle of length $\leq r$ ?

FormalConjectures/ErdosProblems/740.leanErdos740.erdos_7404 linesExact file

1True ↔2  ∀ (V : Type u_1) (G : SimpleGraph V),3    Cardinal.aleph0 ≤ G.chromaticCardinal →4      ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe r

OpenStatement only, no proof