Menger's theorem for adjacent vertices in multigraphs

Let G : Graph α β be a multigraph and let s ≠ t be points. The local vertex form of Menger's theorem does not apply directly when an edge joins s and t, because deleting vertices other than the terminals cannot destroy that one-edge path. This file counts those direct edge identities separately.

If G has finitely many actual vertices and D = {e | G.IsLink e s t} is finite, then after deleting D some set X of k actual vertices separates s from t, while the original graph has k + |D| distinct internally vertex-disjoint paths. The family contains the one-edge path of every e ∈ D; parallel edges therefore contribute separately. Weak duality bounds every internally disjoint path family by |X| + |D| for every such separator.

The attainment theorem is transported from the directed adjacent-terminal theorem for the bidirected arrow family. A directed arrow from s to t is exactly an edge identity in D, and the walk equivalence preserves paths and internal disjointness.

Main results

• Graph.card_le_card_add_card_of_not_reachable_deleteEdges_deleteVerts: weak duality.
• Graph.exists_paths_vertexSeparator_card_add_card_eq: adjacent-terminal Menger in witness form.
• Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths: the predicate form.

References

• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927).
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 9.1.

Weak duality

theorem Graph.card_le_card_add_card_of_not_reachable_deleteEdges_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Fintype { e : β // G.IsLink e s t }] {I : Type u_1} [Fintype I] {P : I → G.Walk s t} (hinj : Function.Injective P) (hP : ∀ (i : I), (P i).IsPath) (hdisj : Pairwise fun (i j : I) => (P i).InternallyDisjoint (P j)) (hs : s ∈ G.vertexSet) {X : Finset α} (hsX : s ∉ X) (htX : t ∉ X) (hX : ¬((G.deleteEdges {e : β | G.IsLink e s t}).deleteVerts ↑X).Reachable s t) : Fintype.card I ≤ X.card + Fintype.card { e : β // G.IsLink e s t }

Weak duality for internally vertex-disjoint paths between possibly adjacent vertices. Let X be a finite set of points avoiding s and t. If deleting X and every edge joining s to t separates the terminals, then a finite family of distinct internally disjoint s–t paths has at most #X plus the number of direct edge identities members.

Attainment

theorem Graph.exists_paths_vertexSeparator_card_add_card_eq {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] [Finite { e : β // G.IsLink e s t }] (hst : s ≠ t) : ∃ (k : ℕ) (P : Fin k ⊕ { e : β // G.IsLink e s t } → G.Walk s t) (X : Finset α), Function.Injective P ∧ (∀ (i : Fin k ⊕ { e : β // G.IsLink e s t }), (P i).IsPath) ∧ (Pairwise fun (i j : Fin k ⊕ { e : β // G.IsLink e s t }) => (P i).InternallyDisjoint (P j)) ∧ (∀ (e : { e : β // G.IsLink e s t }), P (Sum.inr e) = ⋯.toWalk) ∧ ↑X ⊆ G.vertexSet ∧ s ∉ X ∧ t ∉ X ∧ ¬((G.deleteEdges {e : β | G.IsLink e s t}).deleteVerts ↑X).Reachable s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths between possibly adjacent vertices. Let s ≠ t be points of a multigraph with finitely many actual vertices and finitely many edges joining the terminals. For some k, there are distinct internally disjoint paths indexed by Fin k ⊕ {e // G.IsLink e s t}. The path indexed by a direct edge is that one-edge path. There is also a set X of k actual vertices such that deleting X and all direct edges separates s from t.

theorem Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths {α : Type u} {β : Type v} {G : Graph α β} {s t : α} [Finite ↑G.vertexSet] [Finite { e : β // G.IsLink e s t }] (hst : s ≠ t) (k : ℕ) : (∀ (X : Finset α), s ∉ X → t ∉ X → X.card < k → ((G.deleteEdges {e : β | G.IsLink e s t}).deleteVerts ↑X).Reachable s t) ↔ ∃ (P : Fin k ⊕ { e : β // G.IsLink e s t } → G.Walk s t), Function.Injective P ∧ (∀ (i : Fin k ⊕ { e : β // G.IsLink e s t }), (P i).IsPath) ∧ Pairwise fun (i j : Fin k ⊕ { e : β // G.IsLink e s t }) => (P i).InternallyDisjoint (P j)

Menger's theorem for adjacent vertices, predicate form. For distinct points, after deleting every direct edge, every set of fewer than k nonterminal points leaves the terminals reachable exactly when there are distinct internally disjoint paths indexed by Fin k ⊕ {e // G.IsLink e s t}.