Menger's theorem

TheoremMenger's theorem, vertex form#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(s\) and \(t\) be distinct, nonadjacent vertices of \(G\). Then there is a natural number \(n\) with the following two properties. First, there is a set \(C\) of exactly \(n\) vertices with \(s \notin C\) and \(t \notin C\) such that every walk from \(s\) to \(t\) passes through a vertex of \(C\), and every set of vertices with these three properties has at least \(n\) elements. Second, there are \(n\) paths \(P_1, \dots, P_n\) from \(s\) to \(t\) (walks that repeat no vertex) such that every vertex lying on both \(P_i\) and \(P_j\) for some \(i \ne j\) is \(s\) or \(t\), and every finite family of paths from \(s\) to \(t\) with this property has at most \(n\) members. Thus the minimum number of vertices other than \(s\) and \(t\) whose removal separates \(s\) from \(t\) equals the maximum number of pairwise internally disjoint paths from \(s\) to \(t\).

MetaMathlibExt.menger_vertex · 19 lines

theorem menger_vertex :
    ∀ {V : Type*} [Fintype V] (G : SimpleGraph V) (s t : V),
      s ≠ t →
      ¬ G.Adj s t →
      ∃ n : ℕ,
        (∃ C : Finset V,
          C.card = n ∧
          s ∉ C ∧
          t ∉ C ∧
          (∀ p : G.Walk s t, ∃ v ∈ p.support, v ∈ C) ∧
          ∀ C' : Finset V, s ∉ C' → t ∉ C' →
            (∀ p : G.Walk s t, ∃ v ∈ p.support, v ∈ C') → n ≤ C'.card) ∧
        ∃ P : Fin n → G.Walk s t,
          (∀ i, (P i).support.Nodup) ∧
          (∀ i j, i ≠ j → ∀ v, v ∈ (P i).support → v ∈ (P j).support → v = s ∨ v = t) ∧
          ∀ (m : ℕ) (Q : Fin m → G.Walk s t),
            (∀ i, (Q i).support.Nodup) →
            (∀ i j, i ≠ j → ∀ v, v ∈ (Q i).support → v ∈ (Q j).support → v = s ∨ v = t) →
            m ≤ n

Sources

K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115, doi:10.4064/fm-10-1-96-115; statement as in https://en.wikipedia.org/wiki/Menger%27s_theorem (menger-s1).

Used by 1

Used byMenger's theorem for vertex cuts and internally disjoint paths

DefinitionInternally vertex-disjoint paths#✓fully proved

Let \(G\) be a simple graph with vertices \(s\) and \(t\), and let \(P_0, \dots, P_{n-1}\) be a family of paths from \(s\) to \(t\) in \(G\), indexed by \(\{0, \dots, n-1\}\). The family is internally vertex-disjoint when for all indices \(i \ne j\), every vertex lying on both \(P_i\) and \(P_j\) is \(s\) or \(t\).

def IsInternallyVertexDisjointSTPaths {V : Type*} {G : SimpleGraph V}
    {s t : V} {n : ℕ} (paths : Fin n → G.Path s t) : Prop :=
  ∀ i j, i ≠ j → ∀ v, v ∈ (paths i).val.support →
    v ∈ (paths j).val.support → v = s ∨ v = t

Used by 1

Used byMenger's theorem for vertex cuts and internally disjoint paths

DefinitionVertex cuts separating two vertices#✓fully proved

Let \(G\) be a simple graph on a finite vertex set, let \(s\) and \(t\) be vertices of \(G\), and let \(C\) be a set of vertices of \(G\). Then \(C\) is an \(s\)-\(t\) vertex cut when \(s \notin C\), \(t \notin C\), and \(t\) is not reachable from \(s\) in the graph obtained from \(G\) by deleting every edge that has an endpoint in \(C\).

def IsSTVertexCut {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (s t : V) (C : Finset V) : Prop :=
  s ∉ C ∧ t ∉ C ∧
    ¬ (((⊤ : G.Subgraph).deleteVerts (↑C : Set V)).spanningCoe.Reachable s t)

Used by 2

Used byVertex cuts are walk separators · Menger's theorem for vertex cuts and internally disjoint paths

TheoremVertex cuts are walk separators#✓fully proved

Let \(G\) be a simple graph on a finite vertex set, let \(s\) and \(t\) be vertices of \(G\), and let \(C\) be a set of vertices of \(G\). Then \(C\) is an \(s\)-\(t\) vertex cut if and only if \(s \notin C\), \(t \notin C\), and every walk from \(s\) to \(t\) in \(G\) passes through a vertex of \(C\).

theorem isSTVertexCut_iff_walkSeparator {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (s t : V) (C : Finset V) :
    IsSTVertexCut G s t C ↔
      s ∉ C ∧ t ∉ C ∧ ∀ p : G.Walk s t, ∃ v ∈ p.support, v ∈ C

def IsSTVertexCut {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (s t : V) (C : Finset V) : Prop :=
  s ∉ C ∧ t ∉ C ∧
    ¬ (((⊤ : G.Subgraph).deleteVerts (↑C : Set V)).spanningCoe.Reachable s t)

MathlibExt/Combinatorics/Graph/MengerVertex.lean:1952

Uses 1 · Used by 1

Statement usesVertex cuts separating two vertices

Used byMenger's theorem for vertex cuts and internally disjoint paths

TheoremMenger's theorem for vertex cuts and internally disjoint paths#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(s\) and \(t\) be distinct, nonadjacent vertices of \(G\). Then there is a natural number \(k\) such that there exist \(k\) internally vertex-disjoint paths from \(s\) to \(t\) and an \(s\)-\(t\) vertex cut with exactly \(k\) vertices, every family of internally vertex-disjoint paths from \(s\) to \(t\) has at most \(k\) members, and every \(s\)-\(t\) vertex cut has at least \(k\) vertices. In words, the maximum number of internally vertex-disjoint paths from \(s\) to \(t\) equals the minimum size of an \(s\)-\(t\) vertex cut.

theorem menger_vertex_max_min
    {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} [DecidableRel G.Adj]
    (s t : V) (hst : s ≠ t) (hadj : ¬ G.Adj s t) :
    ∃ k : ℕ, ∃ (paths : Fin k → G.Path s t) (C : Finset V),
      IsInternallyVertexDisjointSTPaths paths ∧
      IsSTVertexCut G s t C ∧
      C.card = k ∧
      (∀ {l : ℕ} (paths' : Fin l → G.Path s t),
        IsInternallyVertexDisjointSTPaths paths' → l ≤ k) ∧
      (∀ C' : Finset V, IsSTVertexCut G s t C' → k ≤ C'.card)

def IsInternallyVertexDisjointSTPaths {V : Type*} {G : SimpleGraph V}
    {s t : V} {n : ℕ} (paths : Fin n → G.Path s t) : Prop :=
  ∀ i j, i ≠ j → ∀ v, v ∈ (paths i).val.support →
    v ∈ (paths j).val.support → v = s ∨ v = t

MathlibExt/Combinatorics/Graph/MengerVertex.lean:1946

def IsSTVertexCut {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (s t : V) (C : Finset V) : Prop :=
  s ∉ C ∧ t ∉ C ∧
    ¬ (((⊤ : G.Subgraph).deleteVerts (↑C : Set V)).spanningCoe.Reachable s t)

MathlibExt/Combinatorics/Graph/MengerVertex.lean:1952

Sources

K. Menger, Fund. Math. 10 (1927), DOI 10.4064/fm-10-1-96-115.

Uses 4

Statement usesInternally vertex-disjoint paths · Vertex cuts separating two vertices

Proof usesVertex cuts are walk separators · Menger's theorem, vertex form

DefinitionEdge-disjoint paths#✓fully proved

Let \(G\) be a simple graph with vertices \(s\) and \(t\). A family \(P_0, \dots, P_{n-1}\) of paths from \(s\) to \(t\) in \(G\) is edge-disjoint when, for all indices \(i \ne j\), no edge of \(P_i\) is an edge of \(P_j\).

def IsEdgeDisjointSTPaths {V : Type*} {G : SimpleGraph V}
    {s t : V} {n : ℕ} (paths : Fin n → G.Path s t) : Prop :=
  ∀ i j, i ≠ j → ∀ e : Sym2 V, e ∈ (paths i).val.edges → e ∉ (paths j).val.edges

Used by 1

Used byMenger's theorem for edge cuts and edge-disjoint paths

DefinitionEdge cuts separating two vertices#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(s\) and \(t\) be vertices of \(G\). A finite set \(C\) of unordered pairs of vertices is an \(s\)-\(t\) edge cut when every element of \(C\) is an edge of \(G\) and \(t\) is not reachable from \(s\) in the graph obtained from \(G\) by deleting the edges in \(C\).

def IsSTEdgeCut {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (s t : V) (C : Finset (Sym2 V)) : Prop :=
  (↑C : Set (Sym2 V)) ⊆ G.edgeSet ∧ ¬ (G.deleteEdges (↑C : Set (Sym2 V))).Reachable s t

Used by 1

Used byMenger's theorem for edge cuts and edge-disjoint paths

TheoremMenger's theorem for edge cuts and edge-disjoint paths#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(s\) and \(t\) be distinct vertices of \(G\). Then there is a natural number \(k\) such that there exist \(k\) edge-disjoint paths from \(s\) to \(t\) and an \(s\)-\(t\) edge cut with exactly \(k\) edges, every family of edge-disjoint paths from \(s\) to \(t\) has at most \(k\) members, and every \(s\)-\(t\) edge cut has at least \(k\) edges. In words, the maximum number of edge-disjoint paths from \(s\) to \(t\) equals the minimum size of an \(s\)-\(t\) edge cut.

theorem menger_edge_max_min
    {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} [DecidableRel G.Adj]
    (s t : V) (hst : s ≠ t) :
    ∃ k : ℕ, ∃ (paths : Fin k → G.Path s t) (C : Finset (Sym2 V)),
      IsEdgeDisjointSTPaths paths ∧
      IsSTEdgeCut G s t C ∧
      C.card = k ∧
      (∀ {l : ℕ} (paths' : Fin l → G.Path s t), IsEdgeDisjointSTPaths paths' → l ≤ k) ∧
      (∀ C' : Finset (Sym2 V), IsSTEdgeCut G s t C' → k ≤ C'.card)

def IsEdgeDisjointSTPaths {V : Type*} {G : SimpleGraph V}
    {s t : V} {n : ℕ} (paths : Fin n → G.Path s t) : Prop :=
  ∀ i j, i ≠ j → ∀ e : Sym2 V, e ∈ (paths i).val.edges → e ∉ (paths j).val.edges

MathlibExt/Combinatorics/SimpleGraph/MengerEdge.lean:25

def IsSTEdgeCut {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (s t : V) (C : Finset (Sym2 V)) : Prop :=
  (↑C : Set (Sym2 V)) ⊆ G.edgeSet ∧ ¬ (G.deleteEdges (↑C : Set (Sym2 V))).Reachable s t

MathlibExt/Combinatorics/SimpleGraph/MengerEdge.lean:30

Sources

K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96-115, DOI 10.4064/FM-10-1-96-115.

Uses 2

Statement usesEdge-disjoint paths · Edge cuts separating two vertices

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.