darts_concat — Mathlib

English

When a walk p is extended by an adjacent edge h, the sequence of darts is the old sequence followed by the new dart.

Русский

При добавлении к обходу соседнего ребра h последовательность дротиков наращивается за счёт нового дротика.

LaTeX

$$$(p.\\concat h).\\darts = p.\\darts \\cup \"last\"({(v,w),h})$$$

Lean4

@[simp]
theorem darts_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).darts = p.darts.concat ⟨(v, w), h⟩ :=
  by induction p <;> simp [*, concat_nil]

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