English
Let m ≤ n. For any v : Fin n → α i, any i ∈ Fin n with i ≥ m, and any x ∈ α i, taking the first m elements after updating at i does not change the result: take m h (update v i x) = take m h v.
Русский
Пусть m ≤ n. для любой v : Fin n → α i, для любого i ∈ Fin n с i ≥ m, и для любого x ∈ α i, первые m элементов после обновления в позиции i не изменяются: take m h (update v i x) = take m h v.
LaTeX
$$$\\forall n,\\forall m\\le n,\\forall v:(i:\\mathrm{Fin}(n))\\to \\alpha(i), \\forall i:\\mathrm{Fin}(n), \\forall hi:\\ i \\ge m, \\forall x:\\alpha(i): \\operatorname{take}(m,h)(\\operatorname{update}v\\,i\\,x) = \\operatorname{take}(m,h)v$$$
Lean4
/-- `take` is the same after `update` for indices outside the range of `take`. -/
@[simp]
theorem take_update_of_ge (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin n) (hi : i ≥ m) (x : α i) :
take m h (update v i x) = take m h v := by
ext j
have : castLE h j ≠ i := by
refine ne_of_val_ne ?_
simp only [coe_castLE]
exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)
simp only [take, update_of_ne this]
