menger_directed_max_flow
Provedcombinatoricsgraph-theorynumber-theory
Max-flow min-cut theorem (Ford-Fulkerson): The maximum flow from s to t in a network equals the minimum cut capacity. Proved. Here formalized with integer capacities and flows.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem menger_directed_max_flow (n : ℕ) (hn : 1 ≤ n)
(capacity : Fin n → Fin n → ℕ)
(s t : Fin n) (hst : s ≠ t) :
∃ (max_flow : ℕ),
(∃ flow : Fin n → Fin n → ℕ,
(∀ u v, flow u v ≤ capacity u v) ∧
(∀ u, u ≠ s → u ≠ t → ∑ v, flow u v = ∑ v, flow v u) ∧
max_flow = ∑ v, flow s v) ∧
(∀ (S : Finset (Fin n)), s ∈ S → t ∉ S →
max_flow ≤ ∑ u ∈ S, ∑ v ∉ S, capacity u v) := by
sorrySource