English
For a nodup l and any f, x, y, mapping with f updated at x by y yields an equality with a case split on whether x is in l.
Русский
Для нодуп-листа l и функции f, а также элементов x,y выражение map (update f x y) l равно соответствующему вариативному выражению в зависимости от того, содержится ли x в l.
LaTeX
$$$ [\\DecidableEq \\ α] {l : List α} (hl : l.Nodup) (f : α \\to β) (x : α) (y : β) :\\n \\operatorname{List}.map (\\mathrm{Function.update} f x y) l = \\begin{cases} (\\operatorname{List}.map f l).set (l.idxOf x) y & \\text{if } x \\in l \\\\ \\operatorname{List}.map f l & \\text{if } x \\notin l \\end{cases} . $$$
Lean4
theorem map_update [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) :
l.map (Function.update f x y) = if x ∈ l then (l.map f).set (l.idxOf x) y else l.map f :=
by
induction l with
| nil => simp
| cons hd tl ihl => ?_
rw [nodup_cons] at hl
simp only [mem_cons, map, ihl hl.2]
by_cases H : hd = x
· subst hd
simp [hl.1]
· simp [Ne.symm H, H, ← apply_ite (cons (f hd))]
