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

In [Er71] Erdős suggests that only $n-1$ many cycles and edges are required if we do not require them to be edge-disjoint.

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

1True ↔2  ∀ {V : Type} [inst : Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V),3    ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ ⋃ H ∈ D, H.edgeSet = G.edgeSet ∧ ↑D.card ≤ ↑(Fintype.card V) - 1

OpenStatement only, no proof

Sources

Search problems.science