Vertex connectivity of multigraphs

Vertex connectivity ignores loops and parallel edges. We use the vertex-connectivity predicates and numerical invariant of G.toSimpleGraph, whose carrier consists of the actual vertices of G, not its ambient vertex type. The deletion characterization relates these predicates to native multigraph reachability after deleting ambient vertex sets. Thus witnesses and separators can be expressed with the original vertices and edges even when the ambient types are infinite.

The numerical invariant records exactly the natural thresholds on a nonempty actual vertex set. It is zero on empty and singleton actual vertex sets, and finite whenever the actual vertex set is finite. The simple-graph comparison uses Mathlib's Graph.toSimpleGraphOfSimpleGraphIso.

The conventions follow R. Diestel, Graph Theory, 5th ed., Section 1.4, and the existing SimpleGraph.IsVertexConnected and SimpleGraph.vertexConnectivity interfaces.

@[reducible, inline]

abbrev Graph.IsVertexReachable {α : Type u} {β : Type v} (G : Graph α β) (k : ℕ) (s t : ↑G.vertexSet) : Prop

Actual vertices are k-vertex-reachable when deletion of fewer than k other vertices cannot separate them. Loops and parallel edges do not affect this predicate.

@[reducible, inline]

abbrev Graph.IsVertexConnected {α : Type u} {β : Type v} (G : Graph α β) (k : ℕ) : Prop

A multigraph is k-vertex-connected when its underlying simple graph is. In particular, there must be more than k actual vertices.

@[reducible, inline]

noncomputable abbrev Graph.vertexConnectivity {α : Type u} {β : Type v} (G : Graph α β) : ℕ∞

The vertex connectivity of a multigraph is that of its underlying simple graph.

theorem Graph.isVertexReachable_iff {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {s t : ↑G.vertexSet} : G.IsVertexReachable k s t ↔ ∀ ⦃X : Set α⦄, X.encard < ↑k → ↑s ∉ X → ↑t ∉ X → (G.deleteVerts X).Reachable ↑s ↑t

Vertex reachability can be tested by native vertex deletion. Deleted sets may contain points outside the actual vertex set; those points cannot obstruct reachability.

theorem Graph.IsVertexReachable.zero {α : Type u} {β : Type v} {G : Graph α β} {s t : ↑G.vertexSet} : G.IsVertexReachable 0 s t

Every pair of actual vertices is 0-vertex-reachable.

theorem Graph.IsVertexReachable.anti {α : Type u} {β : Type v} {G : Graph α β} {k l : ℕ} (hkl : k ≤ l) {s t : ↑G.vertexSet} (h : G.IsVertexReachable l s t) : G.IsVertexReachable k s t

Vertex reachability is antitone in its threshold.

@[simp]

theorem Graph.isVertexReachable_one {α : Type u} {β : Type v} {G : Graph α β} {s t : ↑G.vertexSet} : G.IsVertexReachable 1 s t ↔ G.Reachable ↑s ↑t

The threshold 1 for vertex reachability is native multigraph reachability.

theorem Graph.IsVertexReachable.reachable {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (hk : k ≠ 0) {s t : ↑G.vertexSet} (h : G.IsVertexReachable k s t) : G.Reachable ↑s ↑t

A positive vertex-reachability threshold implies native multigraph reachability.

@[simp]

theorem Graph.isVertexConnected_zero {α : Type u} {β : Type v} {G : Graph α β} : G.IsVertexConnected 0 ↔ G.vertexSet.Nonempty

@[simp]

theorem Graph.isVertexConnected_one {α : Type u} {β : Type v} {G : Graph α β} : G.IsVertexConnected 1 ↔ G.Connected ∧ G.vertexSet.Nontrivial

A multigraph is 1-vertex-connected exactly when it is connected and has at least two actual vertices. In particular, a singleton with any number of loops is not 1-connected.

theorem Graph.IsVertexConnected.connected {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (hk : k ≠ 0) (h : G.IsVertexConnected k) : G.Connected

A positive vertex-connectivity threshold implies native multigraph connectedness.

theorem Graph.IsVertexConnected.anti {α : Type u} {β : Type v} {G : Graph α β} {k l : ℕ} (hkl : k ≤ l) (h : G.IsVertexConnected l) : G.IsVertexConnected k

Vertex connectivity is antitone in its threshold.

theorem Graph.IsVertexReachable.mono {α : Type u} {β : Type v} {G H : Graph α β} {k : ℕ} (hGH : G ≤ H) {s t : ↑G.vertexSet} (h : G.IsVertexReachable k s t) : H.IsVertexReachable k ⟨↑s, ⋯⟩ ⟨↑t, ⋯⟩

Adding edges preserves local vertex reachability, with endpoints included into the larger graph's actual vertex set.

theorem Graph.IsVertexConnected.mono {α : Type u} {β : Type v} {G H : Graph α β} {k : ℕ} (hGH : G ≤ H) (hV : G.vertexSet = H.vertexSet) (h : G.IsVertexConnected k) : H.IsVertexConnected k

Global vertex connectivity is monotone under graph inclusion with the same actual vertices. Allowing additional isolated vertices would make this statement false.

theorem Graph.isVertexConnected_iff_le_vertexConnectivity {α : Type u} {β : Type v} {G : Graph α β} [Nonempty ↑G.vertexSet] (k : ℕ) : G.IsVertexConnected k ↔ ↑k ≤ G.vertexConnectivity

On a nonempty actual vertex set, the numerical invariant records exactly the thresholds at which the multigraph is vertex-connected. No finiteness assumption is needed.

theorem Graph.vertexConnectivity_mono {α : Type u} {β : Type v} {G H : Graph α β} (hGH : G ≤ H) (hV : G.vertexSet = H.vertexSet) : G.vertexConnectivity ≤ H.vertexConnectivity

Vertex connectivity is monotone when edges are added without changing the actual vertices.

theorem Graph.vertexConnectivity_ne_top {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] : G.vertexConnectivity ≠ ⊤

A multigraph with finitely many actual vertices has finite vertex connectivity, even when its ambient types or its actual edge set are infinite.

theorem Graph.vertexConnectivity_of_subsingleton {α : Type u} {β : Type v} {G : Graph α β} [Subsingleton ↑G.vertexSet] : G.vertexConnectivity = 0

A multigraph on at most one actual vertex has vertex connectivity zero, independently of its loops and edge multiplicities.

@[simp]

theorem Graph.isVertexReachable_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (k : ℕ) (s t : ↑(ofSimpleGraph H).vertexSet) : (ofSimpleGraph H).IsVertexReachable k s t ↔ H.IsVertexReachable ↑k ↑s ↑t

Local vertex reachability agrees with the simple-graph predicate on Graph.ofSimpleGraph.

@[simp]

theorem Graph.isVertexConnected_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (k : ℕ) : (ofSimpleGraph H).IsVertexConnected k ↔ H.IsVertexConnected ↑k

The vertex-connectivity predicates agree with the simple-graph predicates on Graph.ofSimpleGraph.

@[simp]

theorem Graph.vertexConnectivity_ofSimpleGraph {α : Type u} (H : SimpleGraph α) : (ofSimpleGraph H).vertexConnectivity = H.vertexConnectivity

Passing from a simple graph to a multigraph preserves numerical vertex connectivity, including the empty graph.