English
There is a recursion principle for nonempty vectors: given H(a,t) for any a ∈ α and t ∈ Vector3 α n, we can define a function on Vector3 α (n+1) by consElim(H).
Русский
Существует принцип рекурсии для непустых векторов: задана функция H(a,t) для всех a ∈ α и t ∈ Vector3 α n, тогда можно определить функцию на Vector3 α (n+1) через consElim(H).
LaTeX
$$$ \mathrm{consElim}_{C}(H,v) = H(\mathrm{head}(v), \mathrm{tail}(v))$ for appropriate decomposition $v = \mathrm{head}(v) :: \mathrm{tail}(v)$.$$
Lean4
/-- Recursion principle for a nonempty vector. -/
@[elab_as_elim]
def consElim {C : Vector3 α (n + 1) → Sort u} (H : ∀ (a : α) (t : Vector3 α n), C (a :: t)) (v : Vector3 α (n + 1)) :
C v := by rw [← cons_head_tail v]; apply H
