snoc_comp_rev — Mathlib

English

Reversing then appending at the end is equivalent to prepending after reversing the tail.

Русский

Развёртывание затем добавление в конец эквивалентно добавлению в начало после разворота хвоста.

LaTeX

$$$$\mathrm{Fin.snoc}\ f\ a \circ \mathrm{Fin.rev} = \mathrm{Fin.cons}\ a\ (\mathrm{f} \circ \mathrm{Fin.rev})$$$$

Lean4

theorem snoc_comp_rev {α n} (a : α) (f : Fin n → α) : Fin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev) :=
  funext <| snoc_rev a f

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