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

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement3 of 6

Conlon, Fox, and Sudakov [CFS14] proved that $O_\epsilon(n)$ cycles and edges suffice if $G$ has minimum degree at least $\epsilon n$ , for any $\epsilon>0$ .

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

1∀ ε > 0,2  ∃ f,3    (f =O[Filter.atTop] fun n => ↑n) ∧4      ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),5        ↑G.minDegree ≥ ε * ↑(Fintype.card V) →6          ∃ 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