English
There exists a canonical map dropRepeat that, for every n, takes a function defined on a vector of length n+1 with elements in α and returns a function on the vector of length n, effectively removing one coordinate.
Русский
Существует каноническое отображение dropRepeat, которое для каждого n переводит карту на повторяющемся векторе длины n+1 в вектор длины n, фактически удаляя одну координату.
LaTeX
$$$\\mathrm{dropRepeat}(\\alpha) : \\forall n, \\mathrm{drop}(\\mathrm{repeat}(n+1)\\alpha) \\to \\mathrm{repeat}(n)\\alpha.$$$
Lean4
/-- arrow to remove one element of a `repeat` vector -/
def dropRepeat (α : Type*) : ∀ {n}, drop («repeat» (succ n) α) ⟹ «repeat» n α
| succ _, Fin2.fs i => dropRepeat α i
| succ _, Fin2.fz => fun (a : α) => a
