Residual reachability is equivalent to a simple directed path
ProvedEdmondsKarp.ShortestPath.dirPath_reachablegraph-theorynetwork-flow
Two vertices are related by the reflexive transitive closure of residual adjacency if and only if there is a simple directed residual path between them.
Preamble
import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation open EdmondsKarp.ShortestPath
Formal statement
theorem EdmondsKarp.ShortestPath.dirPath_reachable {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
(f : V → V → ℝ) (u v : V) :
(∃ P, IsDirPath N f u v P) ↔ Relation.ReflTransGen (ResArc N f) u v := by sorrySource
Auxiliary lemmas for the augmenting-path optimality criterion in Edmonds and Karp (1972), §1.1 p. 249. DOI: 10.1145/321694.321699.