Simple Graph

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

TheoremDirac's theorem #

For 2 ≤ k, every set of at most k vertices of a k-vertex-connected simple graph on a finite vertex type lies on a common cycle.

SimpleGraph.IsVertexConnected.exists_isCycle_forall_mem_support.{u} {V : Type u} {G : SimpleGraph V}
  [Finite V] {k : ℕ} (hk : 2 ≤ k) (h : G.IsVertexConnected ↑k) {S : Finset V} (hS : S.card ≤ k) :
  ∃ u c, c.IsCycle ∧ ∀ v ∈ S, v ∈ c.support

Lean

Formalized in Tau Ceti as SimpleGraph.IsVertexConnected.exists_isCycle_forall_mem_support.

Sources

LeanSimpleGraph.IsVertexConnected.exists_isCycle_forall_mem_support

Uses 2

Proof usesMenger's theorem for fans · Whitney's inequality

TheoremThe global form of Menger's theorem #

A simple graph on a finite vertex type with more than k vertices 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.

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

Lean

Formalized in Tau Ceti as SimpleGraph.isVertexConnected_iff_forall_exists_paths.

Sources

LeanSimpleGraph.isVertexConnected_iff_forall_exists_paths

Uses 1

Proof usesMenger's theorem for fans

TheoremLempel–Even–Cederbaum theorem #

On a finite vertex type with at least three vertices, a simple graph G admits an st-numbering for distinct vertices s ≠ t if and only if G ⊔ SimpleGraph.edge s t is 2-vertex-connected.

SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two_sup_edge.{u} {V : Type u} [Fintype V]
  {G : SimpleGraph V} (h3 : 3 ≤ Fintype.card V) {s t : V} (hst : s ≠ t) :
  Nonempty (G.STNumbering s t) ↔ (G ⊔ SimpleGraph.edge s t).IsVertexConnected 2

Lean

Formalized in Tau Ceti as SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two_sup_edge.

Other forms

Lempel–Even–Cederbaum theorem (existence). Formalized in Tau Ceti as SimpleGraph.nonempty_stNumbering_of_isVertexConnected_two_sup_edge.

SimpleGraph.nonempty_stNumbering_of_isVertexConnected_two_sup_edge.{u} {V : Type u} [Fintype V]
  {G : SimpleGraph V} {s t : V} (hst : s ≠ t)
  (hG : (G ⊔ SimpleGraph.edge s t).IsVertexConnected 2) : Nonempty (G.STNumbering s t)

Lempel–Even–Cederbaum theorem for adjacent endpoints. Formalized in Tau Ceti as SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two.

SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two.{u} {V : Type u} [Fintype V]
  {G : SimpleGraph V} (h3 : 3 ≤ Fintype.card V) {s t : V} (hst : G.Adj s t) :
  Nonempty (G.STNumbering s t) ↔ G.IsVertexConnected 2

Sources

LeanSimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two_sup_edge · SimpleGraph.nonempty_stNumbering_of_isVertexConnected_two_sup_edge · SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two

Uses 1

Proof usesMenger's theorem for fans

TheoremMenger's theorem for fans #

Let x be a vertex outside a set U of vertices of a simple graph on a finite vertex type. Some family of k paths, the i-th from x to u i ∈ U with its other vertices outside U, any two of which share only the vertex x, and some set of k vertices other than x meeting every walk from x to a vertex of U exist. By SimpleGraph.card_le_card_of_fan, the fan is then largest and the separator smallest.

SimpleGraph.exists_fan_separator_card_eq.{u} {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V}
  [Finite V] (hx : x ∉ U) :
  ∃ k u P X,
    Function.Injective u ∧
      (∀ (i : Fin k), u i ∈ U) ∧
        (∀ (i : Fin k), (P i).IsPath) ∧
          (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧
            (Pairwise fun i j => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x) ∧
              x ∉ X ∧ (∀ y ∈ U, ∀ (p : G.Walk x y), ∃ v ∈ p.support, v ∈ X) ∧ X.card = k

Lean

Formalized in Tau Ceti as SimpleGraph.exists_fan_separator_card_eq.

Other forms

Menger's theorem for fans, predicate form. Formalized in Tau Ceti as SimpleGraph.forall_exists_walk_iff_exists_fan.

SimpleGraph.forall_exists_walk_iff_exists_fan.{u} {V : Type u} {G : SimpleGraph V} {x : V}
  {U : Finset V} [Finite V] (hx : x ∉ U) (k : ℕ) :
  (∀ (X : Finset V), X.card < k → x ∉ X → ∃ y ∈ U, ∃ p, ∀ v ∈ p.support, v ∉ X) ↔
    ∃ u P,
      Function.Injective u ∧
        (∀ (i : Fin k), u i ∈ U) ∧
          (∀ (i : Fin k), (P i).IsPath) ∧
            (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧
              Pairwise fun i j => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x

Menger's theorem for internally vertex-disjoint paths. Formalized in Tau Ceti as SimpleGraph.exists_paths_vertexSeparator_card_eq.

SimpleGraph.exists_paths_vertexSeparator_card_eq.{u} {V : Type u} {G : SimpleGraph V} {s t : V}
  [Finite V] (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)) ∧
          ∃ (hs : s ∉ X) (ht : t ∉ X),
            ¬(SimpleGraph.induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧ X.card = k

Menger's theorem for internally vertex-disjoint paths between adjacent vertices. Formalized in Tau Ceti as SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq.

SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq.{u} {V : Type u} {G : SimpleGraph V}
  {s t : V} [Finite V] (h : G.Adj s t) :
  ∃ k P X,
    Function.Injective P ∧
      (∀ (i : Fin (k + 1)), (P i).IsPath) ∧
        (Pairwise fun i j => (P i).InternallyDisjoint (P j)) ∧
          P (Fin.last k) = h.toWalk ∧
            ∃ (hs : s ∉ X) (ht : t ∉ X),
              ¬(SimpleGraph.induce (↑X)ᶜ (G.deleteEdges {s(s, t)})).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧
                X.card = k

Menger's theorem for internally vertex-disjoint paths, predicate form. Formalized in Tau Ceti as SimpleGraph.forall_reachable_induce_iff_exists_paths.

SimpleGraph.forall_reachable_induce_iff_exists_paths.{u} {V : Type u} {G : SimpleGraph V} {s t : V}
  [Finite V] (hst : s ≠ t) (hadj : ¬G.Adj s t) (k : ℕ) :
  (∀ (X : Finset V) (hs : s ∉ X) (ht : t ∉ X),
      X.card < k → (SimpleGraph.induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩) ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex reachability. Formalized in Tau Ceti as SimpleGraph.isVertexReachable_iff_exists_paths.

SimpleGraph.isVertexReachable_iff_exists_paths.{u} {V : Type u} {G : SimpleGraph V} [Finite V]
  {s t : V} (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. Formalized in Tau Ceti as SimpleGraph.exists_paths_setSeparator_card_eq.

SimpleGraph.exists_paths_setSeparator_card_eq.{u} {V : Type u} {G : SimpleGraph V} [Finite V]
  (A B : Finset V) :
  ∃ 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), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (Pairwise fun i j => (P i).support.Disjoint (P j).support) ∧
              (∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) ∧ X.card = k

Menger's theorem for vertex-disjoint paths between vertex sets, predicate form. Formalized in Tau Ceti as SimpleGraph.forall_exists_walk_iff_exists_paths.

SimpleGraph.forall_exists_walk_iff_exists_paths.{u} {V : Type u} {G : SimpleGraph V} [Finite V]
  (A B : Finset V) (k : ℕ) :
  (∀ (X : Finset V), X.card < k → ∃ a ∈ A, ∃ b ∈ B, ∃ p, ∀ v ∈ p.support, v ∉ X) ↔
    ∃ 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).support.Disjoint (P j).support

Sources

LeanSimpleGraph.exists_fan_separator_card_eq · SimpleGraph.forall_exists_walk_iff_exists_fan · SimpleGraph.exists_paths_vertexSeparator_card_eq · SimpleGraph.exists_paths_vertexSeparator_card_add_one_eq · SimpleGraph.forall_reachable_induce_iff_exists_paths · SimpleGraph.isVertexReachable_iff_exists_paths · SimpleGraph.exists_paths_setSeparator_card_eq · SimpleGraph.forall_exists_walk_iff_exists_paths

Uses 3 · Used by 4

Proof usesMenger's theorem for vertex-strong arrow families · TauCeti.AuxTerminalHom · Vertex-capacitated Menger's theorem

Used byDirac's theorem · Lempel–Even–Cederbaum theorem · The global form of Menger's theorem · Whitney's theorem with prescribed initial cycle

TheoremVertex-capacitated Menger's theorem #

Let s and t be distinct nonadjacent vertices of a simple graph on a finite vertex type, 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 vertices other than s and t, whose deletion separates s from t, satisfy ∑ v ∈ X, c v = k. By SimpleGraph.card_le_sum_of_not_reachable_induce, the family is then largest and the separator of least weight.

SimpleGraph.exists_paths_vertexSeparator_sum_eq.{u} {V : Type u} {G : SimpleGraph V} {s t : V}
  [Finite V] [DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : ¬G.Adj s t) :
  ∃ k P X,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (∀ (v : V), v ≠ s → v ≠ t → {i | v ∈ (P i).support}.card ≤ c v) ∧
        ∃ (hs : s ∉ X) (ht : t ∉ X),
          ¬(SimpleGraph.induce (↑X)ᶜ G).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ∧ ∑ v ∈ X, c v = k

Lean

Formalized in Tau Ceti as SimpleGraph.exists_paths_vertexSeparator_sum_eq.

Other forms

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

SimpleGraph.exists_paths_setSeparator_sum_eq.{u} {V : Type u} {G : SimpleGraph V} [Finite V]
  [DecidableEq V] (c : V → ℕ) (A B : Finset V) :
  ∃ 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), ∀ v ∈ (P i).support, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (∀ (v : V), {i | v ∈ (P i).support}.card ≤ c v) ∧
              (∀ a ∈ A, ∀ b ∈ B, ∀ (p : G.Walk a b), ∃ v ∈ p.support, v ∈ X) ∧ ∑ v ∈ X, c v = k

Sources

LeanSimpleGraph.exists_paths_vertexSeparator_sum_eq · SimpleGraph.exists_paths_setSeparator_sum_eq

Uses 1 · Used by 1

Proof usesVertex-capacitated Menger's theorem for directed paths

Used byMenger's theorem for fans

TheoremWhitney's inequality #

the vertex connectivity of a simple graph is at most its edge connectivity.

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

Lean

Formalized in Tau Ceti as SimpleGraph.vertexConnectivity_le_edgeConnectivity.

Other forms

Whitney's inequality, predicate form. Formalized in Tau Ceti as SimpleGraph.IsVertexConnected.isEdgeConnected.

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

Sources

LeanSimpleGraph.vertexConnectivity_le_edgeConnectivity · SimpleGraph.IsVertexConnected.isEdgeConnected

Used by 2

Used byWhitney's inequality for multigraphs · Dirac's theorem

TheoremWhitney's theorem with prescribed initial cycle #

For any cycle c in a 2-vertex-connected simple graph on a finite vertex type, there is an open ear decomposition of ⊤ whose initial subgraph is c.toSubgraph.

SimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_initial_eq.{u} {V : Type u}
  {G : SimpleGraph V} [Finite V] (hG : G.IsVertexConnected 2) {u : V} (c : G.Walk u u)
  (hc : c.IsCycle) : ∃ d, d.IsOpen ∧ d.initial = c.toSubgraph

Lean

Formalized in Tau Ceti as SimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_initial_eq.

Sources

LeanSimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_initial_eq

Uses 1

Proof usesMenger's theorem for fans

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Simple Graph

TheoremDirac's theorem#

Lean

Sources

TheoremThe global form of Menger's theorem#

Lean

Sources

TheoremLempel–Even–Cederbaum theorem#

Lean

Other forms

Sources

TheoremMenger's theorem for fans#

Lean

Other forms

Sources

TheoremVertex-capacitated Menger's theorem#

Lean

Other forms

Sources

TheoremWhitney's inequality#

Lean

Other forms

Sources

TheoremWhitney's theorem with prescribed initial cycle#

Lean

Sources

TheoremDirac's theorem #

TheoremThe global form of Menger's theorem #

TheoremLempel–Even–Cederbaum theorem #

TheoremMenger's theorem for fans #

TheoremVertex-capacitated Menger's theorem #

TheoremWhitney's inequality #

TheoremWhitney's theorem with prescribed initial cycle #