length_tail_add_one — Mathlib

English

If p is a nonempty walk, then the length of its tail plus one equals the length of p: p.tail.length + 1 = p.length.

Русский

Если p не пустой ход, то длина хвоста плюс единица равна длине p: p.tail.length + 1 = p.length.

LaTeX

$$$ p.tail.length + 1 = p.length $$$

Lean4

@[simp]
theorem length_tail_add_one {p : G.Walk u v} (hp : ¬p.Nil) : p.tail.length + 1 = p.length := by
  rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp]

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