mapIdx_append_one — Mathlib

English

Mapping with indices distributes over appending a single element: mapIdx f (l ++ [e]) = mapIdx f l ++ [f (l.length) e].

Русский

Отображение с индексами распределяется по конкатенации одного элемента: mapIdx f (l ++ [e]) = mapIdx f l ++ [f (длина(l)) e].

LaTeX

$$$$ \\mathrm{mapIdx}\\ f\\ (l \\ ++\\ [e]) = \\mathrm{mapIdx}\\ f\\ l \\, ++ \\, [f\\ (l.length)\\ e]. $$$$

Lean4

theorem mapIdx_append_one :
    ∀ {f : ℕ → α → β} {l : List α} {e : α}, mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] :=
  mapIdx_concat

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