English
If f is injective, then mapping by f commutes with dedup: (xs.map f).dedup = xs.dedup.map f.
Русский
Если f инективна, то отображение по f commute с удалением повторов: (xs.map f).dedup = xs.dedup.map f.
LaTeX
$$$(\\mathrm{List.map}\ f\\ xs).\\mathrm{dedup} = \\mathrm{List.dedup}(xs)\\.map\ f$$$
Lean4
theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f) (xs : List α) :
(xs.map f).dedup = xs.dedup.map f := by
induction xs with
| nil => simp
| cons x xs ih =>
rw [map_cons]
by_cases h : x ∈ xs
· rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
· rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih, map_cons]
