English
Let xs be a finite list of elements of α. The second symmetric power of xs, denoted xs.sym2, mapped by the canonical equivalence Sym2.equivSym α, equals the second symmetric representation of xs, denoted xs.sym 2. In symbols: (xs.sym2).map (Sym2.equivSym α) = xs.sym 2.
Русский
Пусть xs — конечный список элементов множества α. При отображении через стандартное соответствие Sym2.equivSym α списковая запись xs.sym2 приводится к представлению второго симметрического уровня xs.sym 2: (xs.sym2).map (Sym2.equivSym α) = xs.sym 2.
LaTeX
$$$ (xs.sym2).map (Sym2.equivSym α) = xs.sym 2 $$$
Lean4
theorem sym2_eq_sym_two : xs.sym2.map (Sym2.equivSym α) = xs.sym 2 := by
induction xs with
| nil => simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]
| cons x xs ih =>
rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]
rfl
