English
For any function f: α → β and natural number n, and any list xs : List α, the symmetry operation commutes with map: (xs.map f).sym n = (xs.sym n).map (Sym.map f).
Русский
Пусть f: α → β и натуральное число n; для любого xs : List α выполняется, что симметризация после применения отображения f эквивалентна отображению Sym.map f после симметризации xs: (xs.map f).sym n = (xs.sym n).map (Sym.map f).
LaTeX
$$$ (xs.map f).sym n = (xs.sym n).map (Sym.map f) $$$
Lean4
theorem sym_map {β : Type*} (f : α → β) (n : ℕ) (xs : List α) : (xs.map f).sym n = (xs.sym n).map (Sym.map f) :=
match n, xs with
| 0, _ => by simp only [List.sym]; rfl
| n + 1, [] => by simp [List.sym]
| n + 1, x :: xs =>
by
rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]
simp only [map_map, List.sym, map_append, append_cancel_right_eq]
congr
ext s
simp only [Function.comp_apply, Sym.map_cons]
