Quiver.shortest_path_spec

theorem Quiver.shortest_path_spec : ∀ {V : Type u} [inst : Quiver V] (r : V) [inst_1 : Quiver.RootedConnected r] {a : V} (p : Quiver.Path r a), (Quiver.shortestPath r a).length ≤ p.length

This theorem states that for any rooted and connected quiver (a directed graph), and any two vertices `r` and `a` in this quiver, the length of any given path `p` from `r` to `a` is always greater or equal to the length of the shortest path from `r` to `a`. In other words, one can't find a path from `r` to `a` that is shorter than the shortest path.

More concisely: For any rooted and connected quiver and vertices `r` and `a`, the length of every path from `r` to `a` is greater than or equal to the length of the shortest path from `r` to `a`.