English
Let f : α → β and ts ∈ List α. Then applying map (map f) to permutations ts yields the same as permutations of map f ts: map (map f) (permutations ts) = permutations (map f ts).
Русский
Пусть f : α → β и ts ∈ List α. Тогда применение map (map f) к permutations ts эквивалентно permutations (map f ts).
LaTeX
$$$$\operatorname{map}(\operatorname{map} f)(\operatorname{permutations}\ ts) = \operatorname{permutations}(\operatorname{map} f\ ts)$$$$
Lean4
theorem map_permutations (f : α → β) (ts : List α) : map (map f) (permutations ts) = permutations (map f ts) := by
rw [permutations, permutations, map, map_permutationsAux, map]