vertices_toPath_tail — Mathlib

English

Let e be a morphism i ⟶ j. The path consisting of this single edge has vertex list [i, j], whose tail is the singleton [j]. In particular, tail(vertices(toPath(e))) = [j].

Русский

Пусть e : i ⟶ j. Путь, состоящий только из этого ребра, имеет список вершин [i, j], хвост которого равен [j]. В частности, tail(Vertices(toPath(e))) = [j].

LaTeX

$$$\mathrm{tail}(\mathrm{Vertices}(\mathrm{toPath}(e))) = [j]$$$

Lean4

theorem vertices_toPath_tail {i j : V} (e : i ⟶ j) : e.toPath.vertices.tail = [j] := by simp

Похожие утверждения