English
Let V be a quiver and p a path from a to b. Then the vertex list p.toList forms a chain with respect to the relation R(x,y) that there exists a morphism y ⟶ x; in other words, for every consecutive pair of vertices along p, there is at least one arrow from the later vertex to the earlier vertex.
Русский
Пусть V — квивер, и p — путь от a до b. Тогда список вершин p.toList образует цепь относительно отношения R(x,y) ⇔ существуется морфизм y ⟶ x; другими словами, для каждой пары соседних вершин вдоль пути существует по меньшей мере один переход от следующей вершины к предыдущей.
LaTeX
$$$\\forall {V} (\\mathcal{Q} \\colon\\ odot{Quiver} V) \\; \\forall a,b\\in V \\; (p:Path\\ a\\ b),\\ (p.toList)\\ IsChain\\left(\\lambda x\\ y. \\exists f:\\ y\\to x\\ right)\\right.$$$
Lean4
theorem isChain_toList_nonempty : ∀ {b} (p : Path a b), (p.toList).IsChain (fun x y => Nonempty (y ⟶ x))
| _, nil => .nil
| _, cons nil _ => .singleton _
| _, cons (cons p g) _ => List.IsChain.cons_cons ⟨g⟩ (isChain_toList_nonempty (cons p g))
