Graph

Results named in Tau Ceti's TauCeti.Combinatorics.Graph modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremHakimi's theorem#

A finite multigraph has an orientation with indegree d exactly when d sums to the number of actual edges and every vertex set S has at most d(S) internal edges.

Graph.exists_orientation_indegree_eq_iff.{u, v} {V : Type u} {E : Type v} {G : Graph V E}
  [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] (d : ↑G.vertexSet → ℕ) :
  (∃ o, ∀ (x : ↑G.vertexSet), o.indegree x = d x) ↔
    ∑ x, d x = Fintype.card ↑G.edgeSet ∧
      ∀ (S : Finset ↑G.vertexSet), (G.internalEdges S).card ≤ ∑ x ∈ S, d x

Lean

Formalized in Tau Ceti as Graph.exists_orientation_indegree_eq_iff.

Sources

• Tau Ceti documentation: Graph.exists_orientation_indegree_eq_iff
• Source of Graph.exists_orientation_indegree_eq_iff in TauCeti/Combinatorics/Graph/Orientation/Hakimi.lean

LeanGraph.exists_orientation_indegree_eq_iff

Uses 4

Proof usesHoffman's circulation theorem · Integrality of maximum flows · TauCeti.AuxTerminalHom · TauCeti.residualUpdate

TheoremKőnig's theorem for multiset capacitated matchings#

Let L and R form a bipartition of a multigraph with finitely many actual edges, and let b v : ℕ be a capacity on every actual vertex. Some multiset capacitated matching x and some vertex cover C satisfy ∑ e, x e = ∑ v ∈ C, b v. By Graph.IsCapacitatedMatching.sum_le_sum_of_isVertexCover, the matching is then largest and the cover of least weight.

Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq.{u, v} {α : Type u}
  {β : Type v} {G : Graph α β} [Fintype ↑G.edgeSet] {L R : Finset ↑G.vertexSet}
  (hLR : G.IsBipartition L R) (b : ↑G.vertexSet → ℕ) :
  ∃ x C, G.IsCapacitatedMatching b x ∧ G.IsVertexCover ↑C ∧ ∑ e, x e = ∑ v ∈ C, b v

Lean

Formalized in Tau Ceti as Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq.

Sources

• Tau Ceti documentation: Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq
• Source of Graph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq in TauCeti/Combinatorics/Graph/Matching/Capacitated.lean

LeanGraph.IsBipartition.exists_isCapacitatedMatching_isVertexCover_sum_eq

Uses 1

Proof usesVertex-capacitated Menger's theorem for directed paths

TheoremMenger'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}.

Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths.{u, v} {α : 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,
      Function.Injective P ∧
        (∀ (i : Fin k ⊕ { e // G.IsLink e s t }), (P i).IsPath) ∧
          Pairwise fun i j => (P i).InternallyDisjoint (P j)

Lean

Formalized in Tau Ceti as Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths.

Other forms

Menger's theorem for edge-disjoint paths between vertex sets in a multigraph. Formalized in Tau Ceti as Graph.exists_paths_setEdgeSeparator_card_eq.

Graph.exists_paths_setEdgeSeparator_card_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] {A B : Finset α} (hAB : Disjoint A B) :
  ∃ k a b P F,
    (∀ (i : Fin k), a i ∈ A) ∧
      (∀ (i : Fin k), b i ∈ B) ∧
        (∀ (i : Fin k), (P i).IsPath) ∧
          (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (Pairwise fun i j => (P i).edges.Disjoint (P j).edges) ∧
              ↑F ⊆ G.edgeSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges ↑F).Reachable a b) ∧ F.card = k

Menger's theorem for edge-disjoint paths between vertex sets in a multigraph, predicate form. Formalized in Tau Ceti as Graph.forall_exists_reachable_deleteEdges_iff_exists_paths.

Graph.forall_exists_reachable_deleteEdges_iff_exists_paths.{u, v} {α : Type u} {β : Type v}
  {G : Graph α β} [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] {A B : Finset α} (hAB : Disjoint A B)
  (k : ℕ) :
  (∀ (F : Finset β), F.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteEdges ↑F).Reachable a b) ↔
    ∃ a b P,
      (∀ (i : Fin k), a i ∈ A) ∧
        (∀ (i : Fin k), b i ∈ B) ∧
          (∀ (i : Fin k), (P i).IsPath) ∧
            (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
              Pairwise fun i j => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths between vertex sets in a simple graph. Formalized in Tau Ceti as SimpleGraph.exists_paths_setEdgeSeparator_card_eq.

SimpleGraph.exists_paths_setEdgeSeparator_card_eq.{u} {α : Type u} {G : SimpleGraph α} [Finite α]
  {A B : Finset α} (hAB : Disjoint A B) :
  ∃ k a b P F,
    (∀ (i : Fin k), a i ∈ A) ∧
      (∀ (i : Fin k), b i ∈ B) ∧
        (∀ (i : Fin k), (P i).IsPath) ∧
          (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (Pairwise fun i j => (P i).edges.Disjoint (P j).edges) ∧
              ↑F ⊆ G.edgeSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteEdges ↑F).Reachable a b) ∧ F.card = k

Menger's theorem for edge-disjoint paths between vertex sets in a simple graph, predicate form. Formalized in Tau Ceti as SimpleGraph.forall_exists_reachable_deleteEdges_iff_exists_paths.

SimpleGraph.forall_exists_reachable_deleteEdges_iff_exists_paths.{u} {α : Type u}
  {G : SimpleGraph α} [Finite α] {A B : Finset α} (hAB : Disjoint A B) (k : ℕ) :
  (∀ (F : Finset (Sym2 α)), F.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteEdges ↑F).Reachable a b) ↔
    ∃ a b P,
      (∀ (i : Fin k), a i ∈ A) ∧
        (∀ (i : Fin k), b i ∈ B) ∧
          (∀ (i : Fin k), (P i).IsPath) ∧
            (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
              Pairwise fun i j => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths in a multigraph. Formalized in Tau Ceti as Graph.exists_paths_edgeSeparator_card_eq.

Graph.exists_paths_edgeSeparator_card_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β} {s t : α}
  [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] (hst : s ≠ t) :
  ∃ k P F,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (Pairwise fun i j => (P i).edges.Disjoint (P j).edges) ∧
        ↑F ⊆ G.edgeSet ∧ ¬(G.deleteEdges ↑F).Reachable s t ∧ F.card = k

Menger's theorem for edge-disjoint paths in a multigraph, predicate form. Formalized in Tau Ceti as Graph.isEdgeReachable_iff_exists_paths.

Graph.isEdgeReachable_iff_exists_paths.{u, v} {α : Type u} {β : Type v} {G : Graph α β} {s t : α}
  [Finite ↑G.vertexSet] [Finite ↑G.edgeSet] (hs : s ∈ G.vertexSet) (k : ℕ) :
  G.IsEdgeReachable k s t ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).edges.Disjoint (P j).edges

Menger's theorem for edge-disjoint paths in a simple graph. Formalized in Tau Ceti as SimpleGraph.exists_paths_edgeSeparator_card_eq.

SimpleGraph.exists_paths_edgeSeparator_card_eq.{u} {α : Type u} {G : SimpleGraph α} {s t : α}
  [Finite α] (hst : s ≠ t) :
  ∃ k P F,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (Pairwise fun i j => (P i).edges.Disjoint (P j).edges) ∧
        ↑F ⊆ G.edgeSet ∧ ¬(G.deleteEdges ↑F).Reachable s t ∧ F.card = k

Menger's theorem for edge-disjoint paths in a simple graph, predicate form. Formalized in Tau Ceti as SimpleGraph.isEdgeReachable_iff_exists_paths.

SimpleGraph.isEdgeReachable_iff_exists_paths.{u} {α : Type u} {G : SimpleGraph α} {s t : α}
  [Finite α] (k : ℕ) :
  G.IsEdgeReachable (↑k) s t ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).edges.Disjoint (P j).edges

Menger's theorem for internally vertex-disjoint paths between possibly adjacent vertices. Formalized in Tau Ceti as Graph.exists_paths_vertexSeparator_card_add_card_eq.

Graph.exists_paths_vertexSeparator_card_add_card_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  {s t : α} [Finite ↑G.vertexSet] [Finite { e // G.IsLink e s t }] (hst : s ≠ t) :
  ∃ k P X,
    Function.Injective P ∧
      (∀ (i : Fin k ⊕ { e // G.IsLink e s t }), (P i).IsPath) ∧
        (Pairwise fun i j => (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 in a multigraph. Formalized in Tau Ceti as Graph.exists_paths_vertexSeparator_card_eq.

Graph.exists_paths_vertexSeparator_card_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  {s t : α} [Finite ↑G.vertexSet] (hst : s ≠ t) (hadj : ¬G.Adj s t) :
  ∃ k P X,
    Function.Injective P ∧
      (∀ (i : Fin k), (P i).IsPath) ∧
        (Pairwise fun i j => (P i).InternallyDisjoint (P j)) ∧
          ↑X ⊆ G.vertexSet ∧ s ∉ X ∧ t ∉ X ∧ ¬(G.deleteVerts ↑X).Reachable s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths in a multigraph, predicate form. Formalized in Tau Ceti as Graph.forall_reachable_deleteVerts_iff_exists_paths.

Graph.forall_reachable_deleteVerts_iff_exists_paths.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  {s t : α} [Finite ↑G.vertexSet] (hst : s ≠ t) (hadj : ¬G.Adj s t) (k : ℕ) :
  (∀ (X : Finset α), s ∉ X → t ∉ X → X.card < k → (G.deleteVerts ↑X).Reachable s t) ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)

Menger's theorem for the vertex-reachability predicate. Formalized in Tau Ceti as Graph.isVertexReachable_iff_exists_paths.

Graph.isVertexReachable_iff_exists_paths.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  [Finite ↑G.vertexSet] {s t : ↑G.vertexSet} (hst : s ≠ t) (hadj : ¬G.Adj ↑s ↑t) (k : ℕ) :
  G.IsVertexReachable k s t ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex-disjoint paths between vertex sets in a multigraph. Formalized in Tau Ceti as Graph.exists_paths_setSeparator_card_eq.

Graph.exists_paths_setSeparator_card_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  [Finite ↑G.vertexSet] (A B : Finset α) (hA : ↑A ⊆ G.vertexSet) (hB : ↑B ⊆ G.vertexSet) :
  ∃ k a b P X,
    (∀ (i : Fin k), a i ∈ A) ∧
      (∀ (i : Fin k), b i ∈ B) ∧
        (∀ (i : Fin k), (P i).IsPath) ∧
          (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧
            (Pairwise fun i j => (P i).support.Disjoint (P j).support) ∧
              ↑X ⊆ G.vertexSet ∧ (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) ∧ X.card = k

Menger's theorem for vertex-disjoint paths between vertex sets in a multigraph, predicate form. Formalized in Tau Ceti as Graph.forall_exists_reachable_deleteVerts_iff_exists_paths.

Graph.forall_exists_reachable_deleteVerts_iff_exists_paths.{u, v} {α : Type u} {β : Type v}
  {G : Graph α β} [Finite ↑G.vertexSet] (A B : Finset α) (hA : ↑A ⊆ G.vertexSet)
  (hB : ↑B ⊆ G.vertexSet) (k : ℕ) :
  (∀ (X : Finset α), X.card < k → ∃ a ∈ A, ∃ b ∈ B, (G.deleteVerts ↑X).Reachable a b) ↔
    ∃ a b P,
      (∀ (i : Fin k), a i ∈ A) ∧
        (∀ (i : Fin k), b i ∈ B) ∧
          (∀ (i : Fin k), (P i).IsPath) ∧
            (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧
              Pairwise fun i j => (P i).support.Disjoint (P j).support

Sources

• Tau Ceti documentation: Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths
• Source of Graph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths in TauCeti/Combinatorics/Graph/Connectivity/Menger/Adjacent.lean

LeanGraph.forall_reachable_deleteEdges_deleteVerts_iff_exists_paths · Graph.exists_paths_setEdgeSeparator_card_eq · Graph.forall_exists_reachable_deleteEdges_iff_exists_paths · SimpleGraph.exists_paths_setEdgeSeparator_card_eq · SimpleGraph.forall_exists_reachable_deleteEdges_iff_exists_paths · Graph.exists_paths_edgeSeparator_card_eq · Graph.isEdgeReachable_iff_exists_paths · SimpleGraph.exists_paths_edgeSeparator_card_eq · SimpleGraph.isEdgeReachable_iff_exists_paths · Graph.exists_paths_vertexSeparator_card_add_card_eq · Graph.exists_paths_vertexSeparator_card_eq · Graph.forall_reachable_deleteVerts_iff_exists_paths · Graph.isVertexReachable_iff_exists_paths · Graph.exists_paths_setSeparator_card_eq · Graph.forall_exists_reachable_deleteVerts_iff_exists_paths

Uses 5

Statement usesGraph.Walk

Proof usesMax-flow/min-cut theorem between vertex sets · Menger's theorem for vertex-strong arrow families · Path–cycle decomposition · Vertex-capacitated Menger's theorem for multigraphs

TheoremUndirected max-flow/min-cut theorem#

For nonnegative capacities on the edges of a multigraph and distinct actual vertices s and t, some acyclic s–t flow has value equal to the capacity of some set of actual vertices containing s but not t. By TauCeti.Flow.val_le_edgeCutCapacity this flow is maximum and this cut is minimum.

Graph.exists_flow_val_eq_edgeCutCapacity.{u, v, w} {α : Type u} {β : Type v} {K : Type w}
  {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet]
  [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] [LinearOrder K]
  [IsOrderedAddMonoid K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} (hst : s ≠ t) (hc : 0 ≤ c) :
  ∃ f, f.toFun.IsAcyclic ∧ ∃ S, s ∈ S ∧ t ∉ S ∧ f.val = G.edgeCutCapacity c S

Lean

Formalized in Tau Ceti as Graph.exists_flow_val_eq_edgeCutCapacity.

Other forms

Undirected max-flow/min-cut theorem with integrality. Formalized in Tau Ceti as Graph.exists_flow_val_eq_edgeCutCapacity_mem.

Graph.exists_flow_val_eq_edgeCutCapacity_mem.{u, v, w} {α : Type u} {β : Type v} {K : Type w}
  {G : Graph α β} [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet]
  [(x y : ↑G.vertexSet) → Fintype (G.BidirectedHom x y)] [AddCommGroup K] [LinearOrder K]
  [IsOrderedAddMonoid K] {c : ↑G.edgeSet → K} {s t : ↑G.vertexSet} (hst : s ≠ t) (hc : 0 ≤ c)
  (H : AddSubgroup K) (hcH : ∀ (e : ↑G.edgeSet), c e ∈ H) :
  ∃ f,
    f.toFun.IsAcyclic ∧
      (∀ ⦃x y : ↑G.vertexSet⦄ (a : G.BidirectedHom x y), f.toFun a ∈ H) ∧
        ∃ S, s ∈ S ∧ t ∉ S ∧ f.val = G.edgeCutCapacity c S

Sources

• Tau Ceti documentation: Graph.exists_flow_val_eq_edgeCutCapacity
• Source of Graph.exists_flow_val_eq_edgeCutCapacity in TauCeti/Combinatorics/Graph/Connectivity/Flow.lean

LeanGraph.exists_flow_val_eq_edgeCutCapacity · Graph.exists_flow_val_eq_edgeCutCapacity_mem

Uses 2

Proof usesIntegrality of maximum flows · TauCeti.residualUpdate

TheoremVertex-capacitated Menger's theorem for multigraphs#

Let s ≠ t be points of a multigraph with finitely many actual vertices, joined by no edge, and let c v be a capacity on every vertex. Some family of k paths from s to t, in which every vertex v other than s and t lies on at most c v members, and some set X of actual vertices avoiding s and t, whose deletion leaves s and t unreachable, satisfy ∑ v ∈ X, c v = k. By Graph.card_le_sum_of_not_reachable_deleteVerts, the family is then largest and the separator of least weight.

Graph.exists_paths_vertexSeparator_sum_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β} {s t : α}
  [Finite ↑G.vertexSet] [DecidableEq α] (c : α → ℕ) (hst : s ≠ t) (hadj : ¬G.Adj s t) :
  ∃ k P X,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (∀ (v : α), v ≠ s → v ≠ t → {i | v ∈ (P i).support}.card ≤ c v) ∧
        ↑X ⊆ G.vertexSet ∧ s ∉ X ∧ t ∉ X ∧ ¬(G.deleteVerts ↑X).Reachable s t ∧ ∑ v ∈ X, c v = k

Lean

Formalized in Tau Ceti as Graph.exists_paths_vertexSeparator_sum_eq.

Other forms

Vertex-capacitated Menger's theorem between vertex sets in a multigraph. Formalized in Tau Ceti as Graph.exists_paths_setSeparator_sum_eq.

Graph.exists_paths_setSeparator_sum_eq.{u, v} {α : Type u} {β : Type v} {G : Graph α β}
  [Finite ↑G.vertexSet] [DecidableEq α] (c : α → ℕ) (A B : Finset α) (hA : ↑A ⊆ G.vertexSet)
  (hB : ↑B ⊆ G.vertexSet) :
  ∃ k a b P X,
    (∀ (i : Fin k), a i ∈ A) ∧
      (∀ (i : Fin k), b i ∈ B) ∧
        (∀ (i : Fin k), (P i).IsPath) ∧
          (∀ (i : Fin k), ∀ x ∈ (P i).support, x ≠ a i → x ≠ b i → x ∉ A ∧ x ∉ B) ∧
            (∀ (x : α), {i | x ∈ (P i).support}.card ≤ c x) ∧
              ↑X ⊆ G.vertexSet ∧
                (∀ a ∈ A, ∀ b ∈ B, ¬(G.deleteVerts ↑X).Reachable a b) ∧ ∑ x ∈ X, c x = k

Sources

• Tau Ceti documentation: Graph.exists_paths_vertexSeparator_sum_eq
• Source of Graph.exists_paths_vertexSeparator_sum_eq in TauCeti/Combinatorics/Graph/Connectivity/Menger/Vertex.lean

LeanGraph.exists_paths_vertexSeparator_sum_eq · Graph.exists_paths_setSeparator_sum_eq

Uses 2 · Used by 1

Statement usesGraph.Walk

Proof usesVertex-capacitated Menger's theorem for directed paths

Used byMenger's theorem for adjacent vertices, predicate form

TheoremWhitney's inequality for multigraphs#

vertex connectivity is at most edge connectivity.

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

Lean

Formalized in Tau Ceti as Graph.vertexConnectivity_le_edgeConnectivity.

Other forms

Whitney's inequality for multigraphs, predicate form. Formalized in Tau Ceti as Graph.IsVertexConnected.isEdgeConnected.

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

Sources

• Tau Ceti documentation: Graph.vertexConnectivity_le_edgeConnectivity
• Source of Graph.vertexConnectivity_le_edgeConnectivity in TauCeti/Combinatorics/Graph/Connectivity/Whitney.lean

LeanGraph.vertexConnectivity_le_edgeConnectivity · Graph.IsVertexConnected.isEdgeConnected

Uses 2

Statement usesGraph.Walk

Proof usesWhitney's inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.