edges_append — Mathlib

English

Let p be a walk from u to v and p' be a walk from v to w. Then the edges of the concatenation p followed by p' equal the concatenation of the edge lists: edges(p) ++ edges(p').

Русский

Пусть p — ход из u в v и p' — ход из v в w. Тогда множество рёбер ходов равняется конкатенации списков рёбер: edges(p) ++ edges(p').

LaTeX

$$$ (p.append p').edges = p.edges \;++\; p'.edges $$$

Lean4

@[simp]
theorem edges_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').edges = p.edges ++ p'.edges := by
  simp [edges]

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