Whitney's inequality for multigraphs

Whitney's inequality says that vertex connectivity is at most edge connectivity. This file extends the simple-graph result to multigraphs while retaining edge identities: deleting fewer than k actual edges can destroy at most that many adjacencies of the underlying simple graph. An adjacency is destroyed only when every parallel edge above it is deleted; loops do not affect the underlying simple graph.

The result needs no finiteness assumptions. Together with the incidence bound for edge connectivity, it bounds multigraph vertex connectivity by the number of nonloop edges incident to either of two distinct actual vertices.

The inequality is due to H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150--168. The reduction to the underlying simple graph follows the endpoint selection argument in R. Diestel, Graph Theory, 5th ed., Proposition 1.4.2.

theorem Graph.IsVertexConnected.isEdgeConnected {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (h : G.IsVertexConnected k) : G.IsEdgeConnected k

Whitney's inequality for multigraphs, predicate form: a k-vertex-connected multigraph is k-edge-connected. Parallel edges count separately toward edge connectivity, while loops affect neither side.

theorem Graph.vertexConnectivity_le_edgeConnectivity {α : Type u} {β : Type v} {G : Graph α β} : G.vertexConnectivity ≤ G.edgeConnectivity

Whitney's inequality for multigraphs: vertex connectivity is at most edge connectivity.

theorem Graph.vertexConnectivity_le_nonloopIncidenceCount {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) (hxy : x ≠ y) (hfin : (incidenceSet x \ loopSet x).Finite) : G.vertexConnectivity ≤ ↑(G.nonloopIncidenceCount x)

The vertex connectivity of a multigraph is at most the number of nonloop edges incident to either of two distinct actual vertices. Parallel edges are counted separately.