Erdős Problem 740: Infinitary version of chromatic number and odd cycles

Reference: erdosproblems.com/740

def Erdos740.NoShortOddCycle {V : Type u_1} (G : SimpleGraph V) (r : ℕ) : Prop

A graph avoids odd cycles of length $\leq r$ if it contains no odd cycles of length at most $r$.

Equations

• Erdos740.NoShortOddCycle G r = ∀ (v : V) (c : G.Walk v v), c.IsCycle → Odd c.length → c.length > r

theorem Erdos740.erdos_740 : True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ (H : G.Subgraph), H.coe.chromaticCardinal = G.chromaticCardinal ∧ NoShortOddCycle H.coe r

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$?