append_comp_rev — Mathlib

English

The composition of append with rev equals the composition of reversed components with rev, up to a Fin.cast: append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast (Nat.add_comm ..).

Русский

Складывание append с rev эквивалентно склейке перевёрнутых частей с rev, с поправкой на Fin.cast.

LaTeX

$$$\\mathrm{append}(xs,ys) \\circ \\mathrm{rev} = \\mathrm{append}(ys \\circ \\mathrm{rev}, xs \\circ \\mathrm{rev}) \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add\\_comm}()).$$$

Lean4

theorem append_comp_rev {m n} (xs : Fin m → α) (ys : Fin n → α) :
    append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast (Nat.add_comm ..) :=
  funext <| append_rev xs ys

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