length_reverseAux — Mathlib

English

Let G be a simple graph on a vertex set V. For any walks p : G.Walk u v and q : G.Walk u w, the length of the walk obtained by p.reverseAux(q) equals the sum of the lengths of p and q.

Русский

Пусть G — простой граф над множеством вершин V. Пусть p : G.Walk u v и q : G.Walk u w. Тогда длина обхода, полученного как p.reverseAux(q), равна сумме длин p и q.

LaTeX

$$$\operatorname{length}(p.\mathrm{reverseAux}(q)) = \operatorname{length}(p) + \operatorname{length}(q)$$$

Lean4

@[simp]
protected theorem length_reverseAux {u v w : V} (p : G.Walk u v) (q : G.Walk u w) :
    (p.reverseAux q).length = p.length + q.length := by
  induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, Nat.add_assoc]

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