length_support — Mathlib

English

Let p be a walk from u to v. The length of the support list of p equals the length of p plus 1, i.e., the number of distinct vertices visited equals the number of edges traversed plus one.

Русский

Пусть p — ход из u в v. Длина списка вершин поддержки p равна длине p плюс 1; то есть число посещённых вершин равно числу пройденных рёбер плюс одно.

LaTeX

$$$ |\mathrm{support}(p)| = |p| + 1 $$$

Lean4

@[simp]
theorem length_support {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1 := by induction p <;> simp [*]

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