English
For ho : o = m + n, and vectors u : Fin m → α and v : Fin n → α, the map vecAppend ho u v is equal to the function i ↦ if i < m then u i else v (i − m).
Русский
Для ho: o = m + n и векторов u : Fin m → α и v : Fin n → α, vecAppend ho u v равен функции i ↦ если i < m, то u i, иначе v (i − m).
LaTeX
$$$\\operatorname{vecAppend}(ho,u,v) = \\lambda i:\\mathrm{Fin}(o),\\ \\text{if } i< m \\text{ then } u(i) \\text{ else } v(i-m)$$$
Lean4
theorem vecAppend_eq_ite {α : Type*} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) :
vecAppend ho u v = fun i : Fin o => if h : (i : ℕ) < m then u ⟨i, h⟩ else v ⟨(i : ℕ) - m, by cutsat⟩ :=
by
ext i
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
congr with hi
simp only [eq_rec_constant]
rfl
