length_append — Mathlib

English

Concatenating two walks p and q increases length by the sum of their lengths: length(p.append q) = length(p) + length(q).

Русский

Сложение двух путей p и q увеличивает длину на сумму их длин: length(p.append q) = length(p) + length(q).

LaTeX

$$$$\forall p:\; G.Walk\ u\ v,\ \forall q:\; G.Walk\ v\ w,\ \text{length}(p.append q) = \text{length}(p) + \text{length}(q).$$$$

Lean4

@[simp]
theorem length_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).length = p.length + q.length := by
  induction p with
  | nil => simp
  | cons _ _ ih => simp [ih, add_comm, add_assoc]

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