cons_comp_rev — Mathlib

English

The function that prepends a to a tail and then reverses is the same as the function that snocs a to the reversed tail.

Русский

Функция, которая добавляет в начало a к хвостy и затем разворачивает, равна функции, добавляющей a в конец к развёрнутому хвосту.

LaTeX

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

Lean4

theorem cons_comp_rev {α n} (a : α) (f : Fin n → α) : Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a := by funext i;
  exact cons_rev ..

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