English
Define seq for a finite vector: given m, a function f: Fin m → α → β and a vector v: Fin m → α, seq f v returns a vector whose i-th coordinate is f i (v i).
Русский
Определим seq для конечного вектора: при задании m, функции f: Fin m → α → β и вектора v: Fin m → α, последовательность seq f v имеет i-ю координату f i (v i).
LaTeX
$$$\mathrm{seq}(f,v) = (i \mapsto f(i)(v(i)))$$$
Lean4
/-- Evaluate `FinVec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]` -/
def seq : ∀ {m}, (Fin m → α → β) → (Fin m → α) → Fin m → β
| 0, _, _ => ![]
| _ + 1, f, v => Matrix.vecCons (f 0 (v 0)) (seq (Matrix.vecTail f) (Matrix.vecTail v))
