Triangle inequality for residual distance

Proved

EdmondsKarp.ShortestPath.resDist_triangle

by arexychen · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorynetwork-flow

Residual distance satisfies the triangle inequality, with infinite distance allowed for unreachable pairs.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.resDist_triangle {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (a b c : V) :
    resDist N f a c ≤ resDist N f a b + resDist N f b c := by sorry

Source

Edmonds and Karp (1972), §1.2 p. 251, residual shortest-path distance. DOI: 10.1145/321694.321699.

View graph