Network

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

TheoremThe directed Whitney inequality #

A k-vertex-strong arrow family is k-arc-strong.

TauCeti.IsVertexStrong.isArcStrong.{u, v} {V : Type u} {Q : V → V → Type v} {k : ℕ}
  (h : TauCeti.IsVertexStrong Q k) : TauCeti.IsArcStrong Q k

Lean

Formalized in Tau Ceti as TauCeti.IsVertexStrong.isArcStrong.

Other forms

The directed Whitney inequality, numerical form. Formalized in Tau Ceti as TauCeti.vertexStrongConnectivity_le_arcConnectivity.

TauCeti.vertexStrongConnectivity_le_arcConnectivity.{u, v} {V : Type u} {Q : V → V → Type v} :
  TauCeti.vertexStrongConnectivity Q ≤ TauCeti.arcConnectivity Q

Sources

LeanTauCeti.IsVertexStrong.isArcStrong · TauCeti.vertexStrongConnectivity_le_arcConnectivity

TheoremGeneralized Hoffman's theorem #

Ordered signed bounds admit an assignment of prescribed excess exactly when that excess is balanced and every cut can supply its demand.

TauCeti.ExcessFlow.nonempty_iff.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V]
  [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
  [DecidableEq V] {lo hi : TauCeti.Assignment Q K} {b : V → K} (hlo : lo ≤ hi) :
  Nonempty (TauCeti.ExcessFlow lo hi b) ↔
    ∑ v, b v = 0 ∧
      ∀ (S : Finset V), ∑ v ∈ S, b v + TauCeti.arrowSum lo S Sᶜ ≤ TauCeti.arrowSum hi Sᶜ S

Lean

Formalized in Tau Ceti as TauCeti.ExcessFlow.nonempty_iff.

Sources

LeanTauCeti.ExcessFlow.nonempty_iff

Uses 3 · Used by 1

Proof usesIntegrality of maximum flows · TauCeti.AuxTerminalHom · TauCeti.residualUpdate

Used byHoffman's circulation theorem

TheoremHoffman's circulation theorem #

A bounded circulation exists exactly when every vertex set has total lower bound entering it at most the total upper bound leaving it.

TauCeti.exists_isCirculation_iff.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
  [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
  [DecidableEq V] {lo hi : TauCeti.Assignment Q K} (hlo : lo ≤ hi) :
  (∃ f ∈ Set.Icc lo hi, TauCeti.IsCirculation f) ↔
    ∀ (S : Finset V), TauCeti.arrowSum lo Sᶜ S ≤ TauCeti.arrowSum hi S Sᶜ

Lean

Formalized in Tau Ceti as TauCeti.exists_isCirculation_iff.

Sources

LeanTauCeti.exists_isCirculation_iff

Uses 1 · Used by 1

Proof usesGeneralized Hoffman's theorem

Used byHakimi's theorem

TheoremMax-flow/min-cut theorem between vertex sets #

For disjoint A and B and nonnegative capacities, some A–B flow has value equal to the capacity of some A–B cut. By weak duality (TauCeti.SetFlow.val_le_arrowSum) this flow is maximum and this cut is minimum.

TauCeti.SetFlow.exists_val_eq_arrowSum.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
  [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [LinearOrder K]
  [IsOrderedAddMonoid K] {cap : TauCeti.Assignment Q K} {A B : Finset V} (hAB : Disjoint A B)
  (hcap : 0 ≤ cap) :
  ∃ f S, TauCeti.TerminalCut.IsAdmissible A B S ∧ f.val = TauCeti.arrowSum cap S Sᶜ

Lean

Formalized in Tau Ceti as TauCeti.SetFlow.exists_val_eq_arrowSum.

Sources

LeanTauCeti.SetFlow.exists_val_eq_arrowSum

Uses 3 · Used by 2

Proof usesIntegrality of maximum flows · TauCeti.AuxTerminalHom · TauCeti.residualUpdate

Used byMenger's theorem for adjacent vertices, predicate form · Menger's theorem for vertex-strong arrow families

TheoremMenger's theorem for vertex-strong arrow families #

An arrow family on a finite vertex type is k-vertex-strong exactly when it has more than k vertices and any two distinct vertices s and t are joined by k distinct directed paths pairwise sharing no vertex other than s and t. When there are arrows from s to t, one of these paths may be a single arrow.

TauCeti.isVertexStrong_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v} {k : ℕ}
  [Finite V] :
  TauCeti.IsVertexStrong Q k ↔
    ↑k < ENat.card V ∧
      ∀ ⦃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 TauCeti.isVertexStrong_iff_exists_paths.

Other forms

Menger's theorem for arrow-disjoint directed paths. Formalized in Tau Ceti as TauCeti.exists_paths_arrowSeparator_card_eq.

TauCeti.exists_paths_arrowSeparator_card_eq.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] [∀ (x y : V), Finite (Q x y)] (hst : s ≠ t) :
  ∃ k P F,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (Pairwise fun i j => (P i).arrows.Disjoint (P j).arrows) ∧
        ¬TauCeti.ReachableWithout (↑F) s t ∧ F.card = k

Menger's theorem for arrow-disjoint directed paths between vertex sets. Formalized in Tau Ceti as TauCeti.exists_paths_setArrowSeparator_card_eq.

TauCeti.exists_paths_setArrowSeparator_card_eq.{u, v} {V : Type u} {Q : V → V → Type v} [Finite V]
  [∀ (x y : V), Finite (Q x y)] {A B : Finset V} (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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (Pairwise fun i j => (P i).arrows.Disjoint (P j).arrows) ∧
              (∀ a ∈ A, ∀ b ∈ B, ¬TauCeti.ReachableWithout (↑F) a b) ∧ F.card = k

Menger's theorem for arrow-disjoint directed paths between vertex sets, predicate form. Formalized in Tau Ceti as TauCeti.forall_exists_reachableWithout_iff_exists_paths.

TauCeti.forall_exists_reachableWithout_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v}
  [Finite V] [∀ (x y : V), Finite (Q x y)] {A B : Finset V} (k : ℕ) :
  (∀ (F : Finset ((x : V) × (y : V) × Q x y)),
      F.card < k → ∃ a ∈ A, ∃ b ∈ B, TauCeti.ReachableWithout (↑F) 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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
              Pairwise fun i j => (P i).arrows.Disjoint (P j).arrows

Menger's theorem for arrow-disjoint directed paths, predicate form. Formalized in Tau Ceti as TauCeti.forall_reachableWithout_iff_exists_paths.

TauCeti.forall_reachableWithout_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] [∀ (x y : V), Finite (Q x y)] (k : ℕ) :
  (∀ (F : Finset ((x : V) × (y : V) × Q x y)), F.card < k → TauCeti.ReachableWithout (↑F) s t) ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).arrows.Disjoint (P j).arrows

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

TauCeti.exists_paths_vertexSeparator_card_eq.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] (hst : s ≠ t) (hadj : IsEmpty (Q s t)) :
  ∃ k P X,
    Function.Injective P ∧
      (∀ (i : Fin k), (P i).IsPath) ∧
        (Pairwise fun i j => (P i).InternallyDisjoint (P j)) ∧
          s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding Q (↑X) s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint directed paths between possibly adjacent terminals. Formalized in Tau Ceti as TauCeti.exists_paths_isMixedSeparator_card_eq.

TauCeti.exists_paths_isMixedSeparator_card_eq.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] [Fintype (Q s t)] (hst : s ≠ t) :
  ∃ k P X,
    Function.Injective P ∧
      (∀ (i : Fin k ⊕ Q s t), (P i).IsPath) ∧
        (Pairwise fun i j => (P i).InternallyDisjoint (P j)) ∧
          (∀ (e : Q s t), P (Sum.inr e) = (TauCeti.ArrowWalk.nil s).cons e) ∧
            TauCeti.IsMixedSeparator X (TauCeti.arrowFinset Q s t) s t ∧ X.card = k

Menger's theorem for internally vertex-disjoint directed paths between possibly adjacent terminals, predicate form. Formalized in Tau Ceti as TauCeti.forall_not_isMixedSeparator_iff_exists_paths.

TauCeti.forall_not_isMixedSeparator_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v}
  {s t : V} [Finite V] [Fintype (Q s t)] (hst : s ≠ t) (k : ℕ) :
  (∀ (X : Finset V), X.card < k → ¬TauCeti.IsMixedSeparator X (TauCeti.arrowFinset Q s t) s t) ↔
    ∃ P,
      Function.Injective P ∧
        (∀ (i : Fin k ⊕ Q s t), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)

Menger's theorem for internally vertex-disjoint directed paths, predicate form. Formalized in Tau Ceti as TauCeti.forall_reachableAvoiding_iff_exists_paths.

TauCeti.forall_reachableAvoiding_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] (hst : s ≠ t) (hadj : IsEmpty (Q s t)) (k : ℕ) :
  (∀ (X : Finset V), s ∉ X → t ∉ X → X.card < k → TauCeti.ReachableAvoiding Q (↑X) s t) ↔
    ∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)

Menger's theorem for vertex-disjoint directed paths between vertex sets. Formalized in Tau Ceti as TauCeti.exists_paths_setSeparator_card_eq.

TauCeti.exists_paths_setSeparator_card_eq.{u, v} {V : Type u} {Q : V → V → Type 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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (Pairwise fun i j => (P i).vertices.Disjoint (P j).vertices) ∧
              (∀ a ∈ A, ∀ b ∈ B, ¬TauCeti.ReachableAvoiding Q (↑X) a b) ∧ X.card = k

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

TauCeti.forall_exists_reachableAvoiding_iff_exists_paths.{u, v} {V : Type u} {Q : V → V → Type v}
  [Finite V] (A B : Finset V) (k : ℕ) :
  (∀ (X : Finset V), X.card < k → ∃ a ∈ A, ∃ b ∈ B, TauCeti.ReachableAvoiding Q (↑X) 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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
              Pairwise fun i j => (P i).vertices.Disjoint (P j).vertices

Sources

LeanTauCeti.isVertexStrong_iff_exists_paths · TauCeti.exists_paths_arrowSeparator_card_eq · TauCeti.exists_paths_setArrowSeparator_card_eq · TauCeti.forall_exists_reachableWithout_iff_exists_paths · TauCeti.forall_reachableWithout_iff_exists_paths · TauCeti.exists_paths_vertexSeparator_card_eq · TauCeti.exists_paths_isMixedSeparator_card_eq · TauCeti.forall_not_isMixedSeparator_iff_exists_paths · TauCeti.forall_reachableAvoiding_iff_exists_paths · TauCeti.exists_paths_setSeparator_card_eq · TauCeti.forall_exists_reachableAvoiding_iff_exists_paths

Uses 5 · Used by 3

Proof usesMax-flow/min-cut theorem · Max-flow/min-cut theorem between vertex sets · Path–cycle decomposition · TauCeti.AuxTerminalHom · Vertex-capacitated Menger's theorem for directed paths

Used byMenger's theorem for adjacent vertices, predicate form · Menger's theorem for vertex deletion in a digraph, predicate form · Menger's theorem for fans

TheoremVertex-capacitated Menger's theorem for directed paths #

Let s ≠ t be vertices of an arrow family on a finite vertex type, with no arrow from s to t, and let c v be a capacity on every vertex. Some family of k directed s–t paths, in which every vertex v other than s and t lies on at most c v members, and some set X of vertices avoiding s and t, whose deletion leaves t unreachable from s, satisfy ∑ v ∈ X, c v = k. By TauCeti.card_le_sum_of_not_reachableAvoiding, the family is then largest and the separator of least weight.

TauCeti.exists_paths_vertexSeparator_sum_eq.{u, v} {V : Type u} {Q : V → V → Type v} {s t : V}
  [Finite V] [DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : IsEmpty (Q s t)) :
  ∃ k P X,
    (∀ (i : Fin k), (P i).IsPath) ∧
      (∀ (v : V), v ≠ s → v ≠ t → {i | v ∈ (P i).vertices}.card ≤ c v) ∧
        s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding Q (↑X) s t ∧ ∑ v ∈ X, c v = k

Lean

Formalized in Tau Ceti as TauCeti.exists_paths_vertexSeparator_sum_eq.

Other forms

Vertex-capacitated Menger's theorem for directed paths between vertex sets. Formalized in Tau Ceti as TauCeti.exists_paths_setSeparator_sum_eq.

TauCeti.exists_paths_setSeparator_sum_eq.{u, v} {V : Type u} {Q : V → V → Type 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).vertices, v ≠ a i → v ≠ b i → v ∉ A ∧ v ∉ B) ∧
            (∀ (v : V), {i | v ∈ (P i).vertices}.card ≤ c v) ∧
              (∀ a ∈ A, ∀ b ∈ B, ¬TauCeti.ReachableAvoiding Q (↑X) a b) ∧ ∑ v ∈ X, c v = k

Sources

LeanTauCeti.exists_paths_vertexSeparator_sum_eq · TauCeti.exists_paths_setSeparator_sum_eq

Uses 4 · Used by 5

Proof usesIntegrality of maximum flows · Path–cycle decomposition · TauCeti.AuxTerminalHom · TauCeti.residualUpdate

Used byKőnig's theorem for multiset capacitated matchings · Vertex-capacitated Menger's theorem for multigraphs · Menger's theorem for vertex-strong arrow families · Vertex-capacitated Menger's theorem for a digraph · Vertex-capacitated Menger's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Network

TheoremThe directed Whitney inequality#

Lean

Other forms

Sources

TheoremGeneralized Hoffman's theorem#

Lean

Sources

TheoremHoffman's circulation theorem#

Lean

Sources

TheoremMax-flow/min-cut theorem between vertex sets#

Lean

Sources

TheoremMenger's theorem for vertex-strong arrow families#

Lean

Other forms

Sources

TheoremVertex-capacitated Menger's theorem for directed paths#

Lean

Other forms

Sources

TheoremThe directed Whitney inequality #

TheoremGeneralized Hoffman's theorem #

TheoremHoffman's circulation theorem #

TheoremMax-flow/min-cut theorem between vertex sets #

TheoremMenger's theorem for vertex-strong arrow families #

TheoremVertex-capacitated Menger's theorem for directed paths #