English
Mapping f over the result of permutations'Aux preserves the structure: map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts).
Русский
Отображение f над результатом permutations'Aux сохраняет структуру: map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts).
LaTeX
$$$\forall {\alpha}, {\beta}, {\alpha'}, {\beta'} (f:\, \alpha \to \beta) (t:\, \alpha) (ts:\, List\;\alpha) :\; List.map (List.map f) (List.permutations'Aux t ts) = List.permutations'Aux (f t) (List.map f ts)$$$
Lean4
theorem map_map_permutations'Aux (f : α → β) (t : α) (ts : List α) :
map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts) := by
induction ts with
| nil => rfl
| cons a ts ih => simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]
