Skip to content

Erdős problem 184

Start work

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement4 of 6

In [Er71] Erdős suggests that only n−1n-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
True ↔  ∀ {V : Type} [inst : Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V),    ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ ⋃ H ∈ D, H.edgeSet = G.edgeSet ∧ ↑D.card ≤ ↑(Fintype.card V) - 1
OpenStatement only, no proof