get_take_eq_take_get_comp_cast — Mathlib

English

(l take m).get equals the composition take m h l.get composed with Fin.cast.

Русский

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

LaTeX

$$$(\\text{l.take } m).\\text{get} = (\\operatorname{take} m h (l.get)) \\circ \\mathrm{Fin.cast}(\\mathrm{List.length\\_take\\_of\\_le}\\,h)$$$

Lean4

/-- `Fin.take` intertwines with `List.take` via `List.get`. -/
theorem get_take_eq_take_get_comp_cast {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
    (l.take m).get = take m h l.get ∘ Fin.cast (List.length_take_of_le h) :=
  by
  ext i
  simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, coe_castLE, coe_cast]

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