Robbins' theorem

TheoremRobbins' theorem#✓fully proved

Let \(G\) be a simple graph on a finite nonempty vertex set \(V\). Then \(G\) is connected and, after deleting any single edge of \(G\), every vertex is still reachable from every vertex (that is, \(G\) is 2-edge-connected) if and only if \(G\) has a strongly connected orientation: a relation \(D\) on \(V\) such that \(D(u, v)\) holds only when \(u\) and \(v\) are adjacent, for every edge \(uv\) exactly one of \(D(u, v)\) and \(D(v, u)\) holds, and every vertex \(v\) can be reached from every vertex \(u\) by a finite, possibly empty, sequence of \(D\)-steps.

theorem robbins_theorem_connected {V : Type*} [Finite V] [Nonempty V] (G : SimpleGraph V) :
    (G.Connected ∧
      ∀ u v, G.Adj u v →
        ∀ a b, Relation.ReflTransGen
          (fun x y => G.Adj x y ∧ ¬ ((x = u ∧ y = v) ∨ (x = v ∧ y = u))) a b) ↔
    ∃ D : V → V → Prop, (∀ u v, D u v → G.Adj u v) ∧
      (∀ u v, G.Adj u v → Xor (D u v) (D v u)) ∧
      (∀ u v, Relation.ReflTransGen D u v)

Sources

• H. E. Robbins, "A Theorem on Graphs, with an Application to a Problem of Traffic Control," American Mathematical Monthly 46 (1939), 281–283; https://en.wikipedia.org/wiki/Robbins%27_theorem

Used by 1

Used byRobbins' theorem, allowing the empty graph

TheoremRobbins' theorem, allowing the empty graph#✓fully proved

Let \(G\) be a simple graph on a finite, possibly empty, vertex set \(V\). Then every vertex of \(G\) is reachable from every vertex and, after deleting any single edge of \(G\), every vertex is still reachable from every vertex, if and only if \(G\) has a strongly connected orientation: a relation \(D\) on \(V\) such that \(D(u, v)\) holds only when \(u\) and \(v\) are adjacent, for every edge \(uv\) exactly one of \(D(u, v)\) and \(D(v, u)\) holds, and every vertex \(v\) can be reached from every vertex \(u\) by a finite, possibly empty, sequence of \(D\)-steps.

For nonempty \(V\) the left-hand condition says that \(G\) is 2-edge-connected; for empty \(V\) both sides hold.

theorem robbins_theorem {V : Type*} [Finite V] (G : SimpleGraph V) :
    ((∀ u v, G.Reachable u v) ∧
      ∀ u v, G.Adj u v →
        ∀ a b, Relation.ReflTransGen
          (fun x y => G.Adj x y ∧ ¬ ((x = u ∧ y = v) ∨ (x = v ∧ y = u))) a b) ↔
    ∃ D : V → V → Prop, (∀ u v, D u v → G.Adj u v) ∧
      (∀ u v, G.Adj u v → Xor (D u v) (D v u)) ∧
      (∀ u v, Relation.ReflTransGen D u v)

Sources

• https://en.wikipedia.org/wiki/Robbins%27_theorem

Uses 1

Proof usesRobbins' theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.