English
Taking one element from a Fin(n+1)-indexed vector is given by reindexing with castLE: the first coordinate is v at castLE of the index.
Русский
Получение одного элемента из вектора Fin(n+1)-индексации выражается через перестройку индексов с помощью castLE: первая координата равна v на соответствующем индексе.
LaTeX
$$$\\mathrm{take}\\;1\\; (\\mathrm{Nat}.\\mathrm{le\\_add\\_left}\\ 1\; n)\; v = \\lambda i. v(\\mathrm{castLE}(\\mathrm{Nat}.\\mathrm{le\\_add\\_left}\\ 1\\; n)\, i)$$$
Lean4
@[simp]
theorem take_one {α : Fin (n + 1) → Sort*} (v : (i : Fin (n + 1)) → α i) :
take 1 (Nat.le_add_left 1 n) v = (fun i => v (castLE (Nat.le_add_left 1 n) i)) :=
by
ext i
simp only [take]
