reverse_transfer — Mathlib

English

The reverse of a transferred walk equals the transfer of the reversed walk, up to a simple edge-condition adjustment.

Русский

Обратный обход после переноса равен переносу обращённого обхода с учётом условия ребра.

LaTeX

$$(p.transfer H hp).reverse = p.reverse.transfer H (by simp)$$

Lean4

@[simp]
theorem reverse_transfer (hp) :
    (p.transfer H hp).reverse = p.reverse.transfer H (by simp only [edges_reverse, List.mem_reverse]; exact hp) := by
  induction p with
  | nil => simp
  | cons _ _ ih => simp only [transfer_append, Walk.transfer, reverse_cons, ih]

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