Vertex reachability and vertex connectivity of simple graphs

Two vertices u, v of a simple graph G are k-vertex-reachable, G.IsVertexReachable k u v, when they remain reachable after deleting any set of fewer than k vertices other than u and v; deletion of a set s is the subgraph G.induce sᶜ induced on the remaining vertices. The graph is k-vertex-connected, G.IsVertexConnected k, when it has at least k + 1 vertices (more than k for finite k, infinitely many for k = ⊤) and any two vertices are k-vertex-reachable. Thus a single vertex is 0- but not 1-vertex-connected, and the complete graph on n ≥ 1 vertices is (n - 1)- but not n-vertex-connected. The numerical vertex connectivity G.vertexConnectivity is the supremum in ℕ∞ of the natural thresholds at which G is vertex-connected; it is 0 on the empty vertex type and finite on a finite one.

Adjacent vertices are k-vertex-reachable for every k, since no deletion of other vertices can separate them. Vertex reachability is therefore not transitive, and for adjacent vertices it says nothing beyond the single edge. On a finite vertex type, Menger's theorem identifies k-vertex-reachability of any two vertices with the existence of k paths pairwise sharing no vertex other than their ends; both sides hold trivially for equal or adjacent vertices. On a finite graph with more than k vertices, k-vertex-connectivity is the existence of k such paths between every two distinct vertices, adjacent ones included.

Whitney's inequality compares the two connectivity notions: deleting fewer than k edges can be simulated by deleting fewer than k vertices, one end of each deleted edge, so a k-vertex-connected graph is k-edge-connected and G.vertexConnectivity ≤ G.edgeConnectivity. Together with SimpleGraph.edgeConnectivity_le_minDegree, this bounds vertex connectivity by edge connectivity and edge connectivity by minimum degree on a finite graph with at least two vertices. The inequality is due to H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168; the proof follows R. Diestel, Graph Theory, Proposition 1.4.2, made local to a pair of vertices.

The definitions follow the proposal mathlib4#33355, and their shape and API follow Mathlib's SimpleGraph.IsEdgeReachable and SimpleGraph.IsEdgeConnected. The numerical invariant follows the multigraph Graph.edgeConnectivity in TauCeti.Combinatorics.Graph.Connectivity.EdgeConnectivity, a supremum in ℕ∞ of natural thresholds. The vertex count condition is the usual one, as in R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Section 1.4.

Main definitions

• SimpleGraph.IsVertexReachable G k u v: u and v stay reachable after deleting fewer than k other vertices.
• SimpleGraph.IsVertexConnected G k: G has at least k + 1 vertices, any two of which are k-vertex-reachable.
• SimpleGraph.vertexConnectivity G: the supremum in ℕ∞ of the natural thresholds at which G is vertex-connected.

Main results

• SimpleGraph.isVertexReachable_one, SimpleGraph.isVertexConnected_one: the threshold 1 is reachability, respectively connectedness on at least two vertices.
• SimpleGraph.isVertexConnected_two_iff: 2-vertex-connectivity is connectedness on at least three vertices with no cut vertex.
• SimpleGraph.Iso.isVertexReachable_iff, SimpleGraph.Iso.isVertexConnected_iff: vertex reachability and connectivity are invariant under graph isomorphism.
• SimpleGraph.isVertexConnected_iff: G is k-vertex-connected exactly when it has at least k + 1 vertices and stays preconnected after deleting fewer than k vertices.
• SimpleGraph.isVertexReachable_of_pairwise_internallyDisjoint: k walks pairwise sharing no vertex other than their ends make their ends k-vertex-reachable.
• SimpleGraph.isVertexConnected_iff_le_vertexConnectivity: on a nonempty vertex type, the numerical invariant records exactly the thresholds at which G is vertex-connected.
• SimpleGraph.vertexConnectivity_add_one_le_card: on a nonempty vertex type, κ + 1 is at most the number of vertices, where κ is the vertex connectivity.
• SimpleGraph.vertexConnectivity_top: the complete graph has vertex connectivity ENat.card V - 1.
• SimpleGraph.IsVertexConnected.isEdgeConnected, SimpleGraph.vertexConnectivity_le_edgeConnectivity: Whitney's inequality: a k-vertex-connected graph is k-edge-connected, so vertex connectivity is at most edge connectivity. No finiteness assumption is needed.
• SimpleGraph.isVertexReachable_iff_exists_paths: Menger's theorem, predicate form.
• SimpleGraph.isVertexConnected_iff_forall_exists_paths: the global form of Menger's theorem: on a vertex type V with k < Nat.card V (which forces V to be finite), k-vertex-connectivity is the existence of k distinct internally disjoint paths between every two distinct vertices.
• SimpleGraph.Walk.reachable_induce_coe_of_mem_support, SimpleGraph.Walk.reachable_start_induce_coe: lifting walks in G with toSubgraph ≤ K to reachability in induced subgraphs of K.coe.
• SimpleGraph.reachable_induce_compl_of_mem_verts_toSubgraph_of_encard_le_one: after deleting at most one vertex of K, every remaining vertex of a path in K between two vertices of a subgraph L ≤ K is joined to a remaining vertex of L.
• SimpleGraph.Walk.IsCycle.isVertexConnected_two_toSubgraph: the subgraph traced by a cycle is 2-vertex-connected, with no finiteness assumption.

Implementation notes

The Menger statements are derived from the witness forms in TauCeti.Combinatorics.SimpleGraph.Connectivity.Menger. For adjacent vertices s and t of a k-vertex-connected graph, SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq gives #X + 1 paths together with a set X separating s from t after the edge s(s, t) is deleted. If #X + 1 < k, some vertex w lies outside X ∪ {s, t}, and deleting X together with t, or with s, leaves w reachable from s, or from t, by walks avoiding the edge s(s, t); so X does not separate s from t. Hence k ≤ #X + 1.

Vertex reachability

def SimpleGraph.IsVertexReachable {V : Type u} (G : SimpleGraph V) (k : ℕ∞) (u v : V) : Prop

Two vertices are k-vertex-reachable if they remain reachable after deleting any set of fewer than k vertices other than themselves.

theorem SimpleGraph.isVertexReachable_def {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} : G.IsVertexReachable k u v ↔ ∀ ⦃s : Set V⦄, s.encard < k → ∀ (hu : u ∉ s) (hv : v ∉ s), (induce sᶜ G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

theorem SimpleGraph.isVertexReachable_iff_exists_walk {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} : G.IsVertexReachable k u v ↔ ∀ ⦃s : Set V⦄, s.encard < k → u ∉ s → v ∉ s → ∃ (p : G.Walk u v), ∀ x ∈ p.support, x ∉ s

Vertex reachability through walks: after deleting fewer than k vertices other than u and v, some walk from u to v avoids the deleted vertices.

@[simp]

theorem SimpleGraph.IsVertexReachable.rfl {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u : V} : G.IsVertexReachable k u u

theorem SimpleGraph.IsVertexReachable.refl {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (u : V) : G.IsVertexReachable k u u

theorem SimpleGraph.IsVertexReachable.symm {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} (h : G.IsVertexReachable k u v) : G.IsVertexReachable k v u

theorem SimpleGraph.isVertexReachable_comm {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} : G.IsVertexReachable k u v ↔ G.IsVertexReachable k v u

theorem SimpleGraph.IsVertexReachable.anti {V : Type u} {G : SimpleGraph V} {k l : ℕ∞} {u v : V} (hkl : k ≤ l) (h : G.IsVertexReachable l u v) : G.IsVertexReachable k u v

Vertex reachability at a smaller threshold follows from vertex reachability at a larger one.

theorem SimpleGraph.IsVertexReachable.mono {V : Type u} {G H : SimpleGraph V} {k : ℕ∞} {u v : V} (hGH : G ≤ H) (h : G.IsVertexReachable k u v) : H.IsVertexReachable k u v

Vertex reachability is monotone in the graph.

@[simp]

theorem SimpleGraph.IsVertexReachable.zero {V : Type u} {G : SimpleGraph V} {u v : V} : G.IsVertexReachable 0 u v

@[simp]

theorem SimpleGraph.isVertexReachable_one {V : Type u} {G : SimpleGraph V} {u v : V} : G.IsVertexReachable 1 u v ↔ G.Reachable u v

Reachability is 1-vertex-reachability.

theorem SimpleGraph.IsVertexReachable.reachable {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} (hk : k ≠ 0) (h : G.IsVertexReachable k u v) : G.Reachable u v

theorem SimpleGraph.Adj.isVertexReachable {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} (h : G.Adj u v) : G.IsVertexReachable k u v

Adjacent vertices are k-vertex-reachable for every k.

theorem SimpleGraph.isVertexReachable_of_pairwise_internallyDisjoint {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {P : Fin n → G.Walk u v} (hP : Pairwise fun (i j : Fin n) => (P i).InternallyDisjoint (P j)) : G.IsVertexReachable (↑n) u v

Weak duality for vertex reachability. If there are n walks from u to v pairwise sharing no vertex other than u and v, then u and v are n-vertex-reachable. No finiteness assumption on V is needed.

theorem SimpleGraph.IsVertexReachable.map {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {u v : V} {W : Type u_1} {H : SimpleGraph W} (h : G.IsVertexReachable k u v) (f : G →g H) (hf : Function.Injective ⇑f) : H.IsVertexReachable k (f u) (f v)

Injective graph homomorphisms preserve vertex reachability.

theorem SimpleGraph.Iso.isVertexReachable_iff {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {W : Type u_1} {H : SimpleGraph W} (e : G ≃g H) (u v : V) : H.IsVertexReachable k (e u) (e v) ↔ G.IsVertexReachable k u v

Vertex reachability is invariant under graph isomorphism.

Vertex connectivity

def SimpleGraph.IsVertexConnected {V : Type u} (G : SimpleGraph V) (k : ℕ∞) : Prop

A graph is k-vertex-connected if it has at least k + 1 vertices and any two vertices are k-vertex-reachable. For finite k this asks for more than k vertices; for k = ⊤ it asks for infinitely many.

theorem SimpleGraph.isVertexConnected_def {V : Type u} {G : SimpleGraph V} {k : ℕ∞} : G.IsVertexConnected k ↔ k + 1 ≤ ENat.card V ∧ ∀ (u v : V), G.IsVertexReachable k u v

theorem SimpleGraph.isVertexConnected_iff {V : Type u} {G : SimpleGraph V} {k : ℕ∞} : G.IsVertexConnected k ↔ k + 1 ≤ ENat.card V ∧ ∀ ⦃s : Set V⦄, s.encard < k → (induce sᶜ G).Preconnected

A graph is k-vertex-connected exactly when it has at least k + 1 vertices and stays preconnected after deleting any set of fewer than k vertices.

theorem SimpleGraph.IsVertexConnected.add_one_le_card {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (h : G.IsVertexConnected k) : k + 1 ≤ ENat.card V

theorem SimpleGraph.IsVertexConnected.add_one_le_natCard {V : Type u} {G : SimpleGraph V} [Finite V] {n : ℕ} (h : G.IsVertexConnected ↑n) : n + 1 ≤ Nat.card V

A vertex-connected graph on a finite vertex type has more vertices than its finite connectivity threshold.

theorem SimpleGraph.IsVertexConnected.isVertexReachable {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (h : G.IsVertexConnected k) (u v : V) : G.IsVertexReachable k u v

theorem SimpleGraph.Iso.isVertexConnected_iff {V : Type u} {G : SimpleGraph V} {k : ℕ∞} {W : Type u_1} {H : SimpleGraph W} (e : G ≃g H) : H.IsVertexConnected k ↔ G.IsVertexConnected k

Vertex connectivity is invariant under graph isomorphism.

theorem SimpleGraph.IsVertexConnected.nonempty {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (h : G.IsVertexConnected k) : Nonempty V

theorem SimpleGraph.IsVertexConnected.anti {V : Type u} {G : SimpleGraph V} {k l : ℕ∞} (hkl : k ≤ l) (h : G.IsVertexConnected l) : G.IsVertexConnected k

Vertex connectivity at a smaller threshold follows from vertex connectivity at a larger one.

theorem SimpleGraph.IsVertexConnected.mono {V : Type u} {G H : SimpleGraph V} {k : ℕ∞} (hGH : G ≤ H) (h : G.IsVertexConnected k) : H.IsVertexConnected k

Vertex connectivity is monotone in the graph.

@[simp]

theorem SimpleGraph.isVertexConnected_zero {V : Type u} {G : SimpleGraph V} : G.IsVertexConnected 0 ↔ Nonempty V

A graph is 0-vertex-connected exactly when its vertex type is nonempty.

@[simp]

theorem SimpleGraph.isVertexConnected_one {V : Type u} {G : SimpleGraph V} : G.IsVertexConnected 1 ↔ G.Connected ∧ Nontrivial V

A graph is 1-vertex-connected exactly when it is connected and has at least two vertices.

theorem SimpleGraph.isVertexConnected_two_iff {V : Type u} {G : SimpleGraph V} : G.IsVertexConnected 2 ↔ 3 ≤ ENat.card V ∧ G.Connected ∧ ∀ (v : V), ¬G.IsCutVertex v

A simple graph is 2-vertex-connected exactly when it has at least three vertices, is connected, and has no cut vertex.

theorem SimpleGraph.IsVertexConnected.preconnected {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (hk : k ≠ 0) (h : G.IsVertexConnected k) : G.Preconnected

theorem SimpleGraph.IsVertexConnected.connected {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (hk : k ≠ 0) (h : G.IsVertexConnected k) : G.Connected

@[simp]

theorem SimpleGraph.isVertexConnected_top_iff {V : Type u} {k : ℕ∞} : ⊤.IsVertexConnected k ↔ k + 1 ≤ ENat.card V

The complete graph is k-vertex-connected exactly when it has at least k + 1 vertices.

Subgraph walks and cycle connectivity

theorem SimpleGraph.Walk.reachable_induce_coe_of_mem_support {V : Type u} {G : SimpleGraph V} {K : G.Subgraph} {s : Set ↑K.verts} {a b : V} {r : G.Walk a b} (hrK : r.toSubgraph ≤ K) (hrs : ∀ (z : ↑K.verts), ↑z ∈ r.support → z ∈ s) {p q : ↑s} (hp : ↑↑p ∈ r.support) (hq : ↑↑q ∈ r.support) : (induce s K.coe).Reachable p q

Any two vertices in s : Set K.verts whose underlying vertices lie on a walk r in G with r.toSubgraph ≤ K whose support stays in s are mutually reachable in K.coe.induce s.

theorem SimpleGraph.Walk.reachable_start_induce_coe {V : Type u} {G : SimpleGraph V} {K : G.Subgraph} {s : Set ↑K.verts} {a b : V} (r : G.Walk a b) (hrK : r.toSubgraph ≤ K) (hrs : ∀ (z : ↑K.verts), ↑z ∈ r.support → z ∈ s) {x : ↑K.verts} (hx : ↑x ∈ r.support) : (induce s K.coe).Reachable ⟨⟨a, ⋯⟩, ⋯⟩ ⟨x, ⋯⟩

If a walk r in G has r.toSubgraph ≤ K and every vertex of r in K.verts belongs to s, then every vertex of r is reachable from r's start in K.coe.induce s.

theorem SimpleGraph.reachable_induce_compl_of_mem_verts_toSubgraph_of_encard_le_one {V : Type u} {G : SimpleGraph V} {K L : G.Subgraph} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hpK : p.toSubgraph ≤ K) (hu : u ∈ L.verts) (hv : v ∈ L.verts) (hLK : L ≤ K) {s : Set ↑K.verts} (hs1 : s.encard ≤ 1) {w : ↑K.verts} (hws : w ∉ s) (hwp : ↑w ∈ p.toSubgraph.verts) : ∃ (z : ↑L.verts) (hz : ⟨↑z, ⋯⟩ ∉ s), (induce sᶜ K.coe).Reachable ⟨w, hws⟩ ⟨⟨↑z, ⋯⟩, hz⟩

If a path p with both ends in L lies in K ≥ L and at most one vertex s of K is deleted, every remaining vertex of p is still joined in K to a remaining vertex of L.

theorem SimpleGraph.Walk.IsCycle.isVertexConnected_two_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {c : G.Walk u u} (hc : c.IsCycle) : c.toSubgraph.coe.IsVertexConnected 2

The subgraph traced by any cycle in a simple graph is 2-vertex-connected, with no finiteness assumption.

The numerical invariant

noncomputable def SimpleGraph.vertexConnectivity {V : Type u} (G : SimpleGraph V) : ℕ∞

The vertex connectivity of a simple graph: the supremum in ℕ∞ of the natural thresholds k at which it is k-vertex-connected. It is 0 on the empty vertex type.

theorem SimpleGraph.vertexConnectivity_def {V : Type u} {G : SimpleGraph V} : G.vertexConnectivity = ⨆ (k : ℕ), ⨆ (_ : G.IsVertexConnected ↑k), ↑k

Vertex connectivity is the supremum of the natural connectivity thresholds.

theorem SimpleGraph.Iso.vertexConnectivity_eq {V : Type u} {G : SimpleGraph V} {W : Type u_1} {H : SimpleGraph W} (e : G ≃g H) : H.vertexConnectivity = G.vertexConnectivity

Vertex connectivity is invariant under graph isomorphism.

theorem SimpleGraph.isVertexConnected_iff_le_vertexConnectivity {V : Type u} {G : SimpleGraph V} [Nonempty V] (k : ℕ) : G.IsVertexConnected ↑k ↔ ↑k ≤ G.vertexConnectivity

On a nonempty vertex type, vertex connectivity records exactly the thresholds at which the graph is vertex-connected.

@[simp]

theorem SimpleGraph.vertexConnectivity_of_isEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] : G.vertexConnectivity = 0

theorem SimpleGraph.vertexConnectivity_mono {V : Type u} {G H : SimpleGraph V} (hGH : G ≤ H) : G.vertexConnectivity ≤ H.vertexConnectivity

Vertex connectivity is monotone in the graph.

theorem SimpleGraph.vertexConnectivity_le_card {V : Type u} {G : SimpleGraph V} : G.vertexConnectivity ≤ ENat.card V

@[simp]

theorem SimpleGraph.vertexConnectivity_ne_top {V : Type u} {G : SimpleGraph V} [Finite V] : G.vertexConnectivity ≠ ⊤

The vertex connectivity of a graph on a finite vertex type is finite.

theorem SimpleGraph.vertexConnectivity_add_one_le_card {V : Type u} {G : SimpleGraph V} [Nonempty V] : G.vertexConnectivity + 1 ≤ ENat.card V

On a nonempty vertex type, the vertex connectivity plus one is at most the number of vertices, so the vertex connectivity is strictly less than it when V is finite.

theorem SimpleGraph.vertexConnectivity_le_card_sub_one {V : Type u} {G : SimpleGraph V} : G.vertexConnectivity ≤ ENat.card V - 1

Vertex connectivity is at most the number of vertices minus one.

@[simp]

theorem SimpleGraph.vertexConnectivity_of_subsingleton {V : Type u} {G : SimpleGraph V} [Subsingleton V] : G.vertexConnectivity = 0

A graph on at most one vertex has vertex connectivity zero.

@[simp]

theorem SimpleGraph.vertexConnectivity_top {V : Type u} : ⊤.vertexConnectivity = ENat.card V - 1

The complete graph on V has vertex connectivity ENat.card V - 1.

Menger's theorem

theorem SimpleGraph.isVertexReachable_iff_exists_paths {V : Type u} {G : SimpleGraph V} [Finite V] {s t : V} (k : ℕ) : G.IsVertexReachable (↑k) s t ↔ ∃ (P : Fin k → G.Walk s t), (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex reachability. Two vertices s and t of a simple graph on a finite vertex type are k-vertex-reachable exactly when there are k paths from s to t pairwise sharing no vertex other than s and t.

theorem SimpleGraph.isVertexConnected_iff_forall_exists_paths {V : Type u} {G : SimpleGraph V} {k : ℕ} (hk : k < Nat.card V) : G.IsVertexConnected ↑k ↔ ∀ (s t : V), s ≠ t → ∃ (P : Fin k → G.Walk s t), Function.Injective P ∧ (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun (i j : Fin k) => (P i).InternallyDisjoint (P j)

The global form of Menger's theorem. A simple graph on a vertex type V with k < Nat.card V (which forces V to be finite) is k-vertex-connected exactly when every two distinct vertices s and t, adjacent or not, are joined by k distinct paths pairwise sharing no vertex other than s and t.

Whitney's inequality

theorem SimpleGraph.IsVertexConnected.isEdgeConnected {V : Type u} {G : SimpleGraph V} {k : ℕ∞} (h : G.IsVertexConnected k) : G.IsEdgeConnected k

Whitney's inequality, predicate form: a k-vertex-connected graph is k-edge-connected.

theorem SimpleGraph.vertexConnectivity_le_edgeConnectivity {V : Type u} {G : SimpleGraph V} : G.vertexConnectivity ≤ G.edgeConnectivity

Whitney's inequality: the vertex connectivity of a simple graph is at most its edge connectivity.