English
For is and ts, the permutations of the concatenation is ++ ts equals the map of the permutations of is appended with ts, together with the permutations of ts with is.reverse appended after. In symbols: permutations (is ++ ts) = (permutations is).map (· ++ ts) ++ permutationsAux ts is.reverse.
Русский
Для списков is и ts перестановки объединения is ++ ts равны отображению перестановок is на добавление ts, а также перестановкам ts с is.reverse, присоединённым после. В общем виде: permutations (is ++ ts) = (permutations is).map (λ s, s ++ ts) ++ permutationsAux ts is.reverse.
LaTeX
$$$$\operatorname{permutations}(is ++ ts) = (\operatorname{permutations} is).\operatorname{map}(\lambda s. s ++ ts) \; ++ \operatorname{permutationsAux}\ ts\ (is.reverse)$$$$
Lean4
theorem permutations_append (is ts : List α) :
permutations (is ++ ts) = (permutations is).map (· ++ ts) ++ permutationsAux ts is.reverse := by
simp [permutations, permutationsAux_append]
