Nash-Williams arboricity theorem

DefinitionArboricity colorings#✓fully proved

Let \(G\) be a simple graph and \(k\) a natural number. A labeling of the edges of \(G\) with labels in \(\{0, 1, \dots, k - 1\}\) is an arboricity coloring when, for each label \(i\), the graph on the vertices of \(G\) whose edges are the edges of \(G\) labeled \(i\) is acyclic, that is, a forest.

def IsArboricityColoring {V : Type*} {G : SimpleGraph V} {k : ℕ}
    (C : G.EdgeLabeling (Fin k)) : Prop :=
  ∀ i : Fin k, (C.labelGraph i).IsAcyclic

Used by 1

Used byNash–Williams arboricity theorem

TheoremNash–Williams arboricity theorem#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(k\) be a natural number. Then \(G\) has an arboricity coloring with \(k\) labels, that is, its edges can be labeled with \(k\) labels so that the edges of each label form a forest, if and only if for every nonempty set \(U \subseteq V\), the number of edges of \(G\) with both endpoints in \(U\) is at most \(k(|U| - 1)\).

theorem nash_williams_arboricity
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) :
    (∃ C : G.EdgeLabeling (Fin k), IsArboricityColoring C) ↔
      ∀ (U : Finset V), U.Nonempty →
        (G.induce (U : Set V)).edgeFinset.card ≤ k * (U.card - 1)

Sources

• C. St. J. A. Nash-Williams, J. London Math. Soc. 39 (1964), DOI 10.1112/jlms/s1-39.1.12.

Uses 1

Statement usesArboricity colorings

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.