English
For any f: α → β, and any ts, is ∈ List α, mapping f twice over permutationsAux ts is equal to permutationsAux of the mapped ts and mapped is: map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is).
Русский
Пусть f : α → β, и любые ts, is ∈ List α. Тогда map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is).
LaTeX
$$$$\operatorname{map}(\operatorname{map} f)(\operatorname{permutationsAux}\ ts\ is) = \operatorname{permutationsAux}(\operatorname{map} f\ ts)(\operatorname{map} f\ is)$$$$
Lean4
theorem map_permutationsAux (f : α → β) :
∀ ts is : List α, map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is) :=
by
refine permutationsAux.rec (by simp) ?_
introv IH1 IH2; rw [map] at IH2
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations, flatMap_map, IH1,
append_assoc, permutationsAux_cons, flatMap_cons, ← IH2, map_flatMap]
