English
Mapping f over a foldl erase-list equals folding with erase by f(a) at each step, under injectivity of f.
Русский
Поскольку отображение через f сохраняет инъективность, отображение через f над результатом обобщённого свёртывания с удалением эквивалентно свёртыванию с удалением через f(a) на каждом шаге.
LaTeX
$$$ \\text{map}\\ f\\ (\\text{foldl}\\ \\text{List.erase}\\ l_1\\ l_2) = \\text{foldl}\\ (\\lambda l\\ a. l.\\text{erase} (f\\ a))\\ (\\text{map}\\ f\\ l_1)\\ l_2 $$$
Lean4
theorem map_foldl_erase [DecidableEq β] {f : α → β} (finj : Injective f) {l₁ l₂ : List α} :
map f (foldl List.erase l₁ l₂) = foldl (fun l a => l.erase (f a)) (map f l₁) l₂ := by
induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]
