vertices_length — Mathlib

English

For any path p from a to b, the length of the vertices list equals the length of the path plus one.

Русский

Для любого пути p от a к b длина списка вершин равна длине пути плюс единица.

LaTeX

$$vertices_length$$

Lean4

/-- The length of vertices list equals path length plus one -/
@[simp]
theorem vertices_length {V : Type*} [Quiver V] {a b : V} (p : Path a b) : p.vertices.length = p.length + 1 := by
  induction p with
  | nil => simp
  | cons p' e ih => simp [vertices_cons, length_cons, ih]

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