English
Let m ≤ n' ≤ n and v : (i : Fin n) → α i. Then taking the first m elements of the first n' elements of v equals taking the first m elements of v with the combined bound h'' := Nat.le_trans h h'.
Русский
Пусть m ≤ n' ≤ n и v : (i : Fin n) → α i. Тогда взятие первых m элементов из первых n' элементов v равняется взятию первых m элементов v с объединенным пределом.
LaTeX
$$$\\mathrm{take}_m(h)\\bigl(\\mathrm{take}_{n'}(h')\,v\\bigr) = \\mathrm{take}_m(\\mathrm{Nat.le\\_trans}(h,h'))\,v$$$
Lean4
@[simp]
theorem take_take {m n' : ℕ} (h : m ≤ n') (h' : n' ≤ n) (v : (i : Fin n) → α i) :
take m h (take n' h' v) = take m (Nat.le_trans h h') v :=
rfl
