English
Let l be a finite list of elements of α and f: α → β be injective. Then applying the destination-of-duplication operator to l with respect to ≠ and then mapping by f equals applying map f to l first and then applying the destination-of-duplication with respect to ≠.
Русский
Пусть l — конечный список элементов из α, а f: α → β инъективен. Тогда применение операции destutter (с ≠) к l затем отображение f эквивалентно применению отображения f к l затем destutter (с ≠).
LaTeX
$$$\\text{map}_f(\\text{destutter}(l, \\neq)) = \\text{destutter}(\\text{map}_f(l), \\neq)$$$
Lean4
/-- For a injective function `f`, `destutter' (·≠·)` commutes with `map f`. -/
theorem map_destutter_ne {f : α → β} (h : Injective f) [DecidableEq α] [DecidableEq β] :
(l.destutter (· ≠ ·)).map f = (l.map f).destutter (· ≠ ·) :=
map_destutter fun _ _ _ _ ↦ h.ne_iff.symm
