edges_concat — Mathlib

English

Let G be a simple graph. If p is a walk from u to v and h is an edge from v to w, then the list of edges of the extended walk p concatenated with h equals the original list of edges of p with the edge (v,w) appended.

Русский

Пусть G — простый граф. Пусть p — путь (ход) из u в v и h — ребро между вершинами v и w. Тогда список рёбер пройденного пути p.concat h равен списку рёбер p с добавлением ребра (v,w).

LaTeX

$$$ (p \concat h).edges = p.edges \cup \{ s(v,w) \} $$$

Lean4

@[simp]
theorem edges_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).edges = p.edges.concat s(v, w) := by
  simp [edges]

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