getElem_map_rev — Mathlib

English

For any f, l, and index n with h, we have f(l[n]) = (map f l)[n] with the appropriate index adjustment.

Русский

Для преобразования отображения f в список: f(l[n]) = (map f l)[n] при соответствующем ограничении индекса.

LaTeX

$$$ f(l[n]) = (map\ f\ l)[n] \text{ for } n < l.length $$$

Lean4

/-- A version of `getElem_map` that can be used for rewriting. -/
theorem getElem_map_rev (f : α → β) {l} {n : Nat} {h : n < l.length} :
    f l[n] = (map f l)[n]'((l.length_map f).symm ▸ h) :=
  Eq.symm (getElem_map _)

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