mapIdx_eq_ofFn — Mathlib

English

The mapIdx of a list can be described by a function on Fin(n) that takes the nth element via the list's get function.

Русский

Отображение по индексу списка можно описать функцией на Fin(n), которая берет n-й элемент через get.

LaTeX

$$$$ \mathrm{mapIdx}\ f \ l = \mathrm{ofFn}\ (\lambda i: \mathrm{Fin}\ l.length \mapsto f (i : \mathbb{N}) (l.get i)). $$$$

Lean4

theorem mapIdx_eq_ofFn (l : List α) (f : ℕ → α → β) : l.mapIdx f = ofFn fun i : Fin l.length ↦ f (i : ℕ) (l.get i) := by
  induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]

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