transfer_append — Mathlib

English

Transferring the concatenation of walks equals concatenation of transfers with a suitable hp.

Русский

Перенос конкатенации обходов равен конкатенации переносов с подходящим hp.

LaTeX

$$(p.append q).transfer H hpq = (p.transfer H h1).append (q.transfer H h2)$$

Lean4

@[simp]
theorem transfer_append {w : V} (q : G.Walk v w) (hpq) :
    (p.append q).transfer H hpq =
      (p.transfer H fun e he => hpq _ (by simp [he])).append (q.transfer H fun e he => hpq _ (by simp [he])) :=
  by
  induction p with
  | nil => simp
  | cons _ _ ih => simp only [Walk.transfer, cons_append, ih]

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