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 statement1 of 6

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

FormalConjectures/ErdosProblems/184.leanErdos184.erdos_1844 linesExact file

1∃ f,2  (f =O[Filter.atTop] fun n => ↑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)

OpenStatement only, no proof

Sources

Search problems.science