length_copy — Mathlib

English

Copying a walk with equal endpoints preserves length: if u = u' and v = v', then copy(p,u,v) has the same length as p.

Русский

Копирование пути с теми же начальными и конечными вершинами сохраняет длину: если u = u' и v = v', то копия(p) имеет ту же длину, что и p.

LaTeX

$$$$\forall p\, \forall u,u',\forall v,v',\ (p.copy\ u' v')\text{ length} = \text{length}(p).$$$$

Lean4

@[simp]
theorem length_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).length = p.length :=
  by
  subst_vars
  rfl

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