English
For an injective map f, mapping f after erasing a from l equals erasing f(a) after mapping f over l.
Русский
При инъективном отображении f отображение через f после удаления a из списка l эквивалентно удалению f(a) после отображения f над l.
LaTeX
$$$ \\text{map}\\ f\\ (l.\\text{erase } a) = (\\text{map}\\ f\\ l).\\text{erase } (f\\ a) $$$
Lean4
theorem map_erase [DecidableEq β] {f : α → β} (finj : Injective f) {a : α} (l : List α) :
map f (l.erase a) = (map f l).erase (f a) :=
by
have this : (a == ·) = (f a == f ·) := by ext b; simp [finj.eq_iff]
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]; rfl
