map_insertIdx — Mathlib

English

Mapping after inserting at n equals inserting at n after mapping the list.

Русский

После вставки на позиции n отображение в результат применимо к вставке в отображенном списке.

LaTeX

$$$\\operatorname{map} f (l.insertIdx n a) = (\\operatorname{map} f l).insertIdx n (f a)$$$

Lean4

theorem map_insertIdx (f : α → β) (l : List α) (n : ℕ) (a : α) :
    (l.insertIdx n a).map f = (l.map f).insertIdx n (f a) := by
  simpa only [pmap_eq_map] using (insertIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) trivial).symm

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