English
Let α be a family over Fin(n+1). For any m ≤ n and v : (i : Fin(n+1)) → α i, taking the first m elements of the initial segment init v equals taking the first m elements of v with bound Nat.le_succ_of_le h.
Русский
Пусть α—семейство над Fin(n+1). Для любого m ≤ n и v : (i : Fin(n+1)) → α i, взятие первых m элементов из начального отрезка init v равно взятию первых m элементов из v с границей Nat.le_succ_of_le h.
LaTeX
$$$\\mathrm{take}_m(h)(\\mathrm{init}\,v) = \\mathrm{take}_m(\\mathrm{Nat.le\\_succ\\_of\\_le}\, h)\,v$$$
Lean4
@[simp]
theorem take_init {α : Fin (n + 1) → Sort*} (m : ℕ) (h : m ≤ n) (v : (i : Fin (n + 1)) → α i) :
take m h (init v) = take m (Nat.le_succ_of_le h) v :=
rfl
