English
Let f: α → β and l: List α. Then erasing the nth element after mapping f over l is the same as mapping f over the list obtained by erasing the nth element of l: (map f l).eraseIdx n = (l.eraseIdx n).map f.
Русский
Пусть f: α → β и l : List α. Тогда удаление элемента с индексом n после отображения f на l эквивалентно отображению f над списком, полученным удалением элемента с индексом n из l: (map f l).eraseIdx n = (l.eraseIdx n).map f.
LaTeX
$$$(\operatorname{map} f\, l).\operatorname{eraseIdx} n = (l\operatorname{eraseIdx} n)\operatorname{map} f$$$
Lean4
/-- Erasing an index commutes with `List.map`. -/
theorem eraseIdx_map (f : α → β) (l : List α) (n : ℕ) : (map f l).eraseIdx n = (l.eraseIdx n).map f := by
simpa only [pmap_eq_map] using eraseIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) n
