Erdős problem 184 · problems.science

Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement6 of 6

Erdős and Gallai [EGP66] proved that $O(n \log n)$ many cycles and edges suffices.

FormalConjectures/ErdosProblems/184.leanErdos184.erdos_184.variants.n_log_n4 linesExact file

1∃ f,2  (f =O[Filter.atTop] fun n => ↑n * Real.log ↑n) ∧3    ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),4      ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

SolvedStatement only, no proof

Sources

Search problems.science