Consecutive path arcs are a relational chain
ProvedEdmondsKarp.ShortestPath.pathArcs_chaingraph-theorynetwork-flow
For any binary relation on vertices, every consecutive pair in a list satisfies the relation if and only if that list is a chain for the relation.
Preamble
import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation open EdmondsKarp.ShortestPath
Formal statement
theorem EdmondsKarp.ShortestPath.pathArcs_chain {V : Type} [Fintype V] [DecidableEq V] (R : V → V → Prop) (P : List V) :
(∀ e ∈ pathArcs P, R e.1 e.2) ↔ P.IsChain R := by sorrySource
Auxiliary directed-path lemmas for Edmonds and Karp (1972), §1.1 p. 249 and §1.2 pp. 251–252. DOI: 10.1145/321694.321699.