reverse_append — Mathlib

English

The reverse of the concatenation of two compositions equals the concatenation of their reverses in the opposite order (up to index reindexing).

Русский

Разворот конкатенации двух композиции равен конкатенации их обратных в противоположном порядке (с переиндексацией).

LaTeX

$$$\\mathrm{reverse}(\\mathrm{append}(c_1,c_2)) = \\mathrm{append}(\\mathrm{reverse}(c_2),\\mathrm{reverse}(c_1)).$$$

Lean4

theorem reverse_append (c₁ : Composition m) (c₂ : Composition n) :
    reverse (append c₁ c₂) = (append c₂.reverse c₁.reverse).cast (add_comm _ _) :=
  Composition.ext <| by simp

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