length_concat — Mathlib

English

Concatenating a walk with a single-edge walk increases length by 1: length(p.concat h) = length(p) + 1.

Русский

Конкатенация пути с одноборученным (односвязным) путём увеличивает длину на 1: length(p.concat h) = length(p) + 1.

LaTeX

$$$$\forall p:\; G.Walk\ u\ v,\forall h:\; G.Adj v w,\ \text{length}(p.concat h) = \text{length}(p) + 1.$$$$

Lean4

@[simp]
theorem length_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).length = p.length + 1 :=
  length_append _ _

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