get_take_ofFn_eq_take_comp_cast — Mathlib

English

((List.ofFn v).take m).get equals take m h v composed with Fin.cast.

Русский

((List.ofFn v).take m).get равно take m h v после композиции Fin.cast.

LaTeX

$$$((\\operatorname{List.ofFn} v).take m).\\text{get} = \\operatorname{take} m h v \\circ \\mathrm{Fin.cast}(\\mathrm{by simp [h]})$$$

Lean4

/-- Alternative version of `take_eq_take_list_get` with `v : Fin n → α` instead of `l : List α`. -/
theorem get_take_ofFn_eq_take_comp_cast {α : Type*} {m : ℕ} (v : Fin n → α) (h : m ≤ n) :
    ((List.ofFn v).take m).get = take m h v ∘ Fin.cast (by simp [h]) :=
  by
  ext i
  simp [castLE]

Похожие утверждения