English
Similarly for image under f: (s.image f).sym2 = s.sym2.image (Sym2.map f).
Русский
Аналогично для отображения: (s.image f).sym2 = s.sym2.image (Sym2.map f).
LaTeX
$$$(s.image f)^{\!\text{sym2}} = s^{\!\text{sym2}}.image(\text{Sym2.map } f)$$$
Lean4
theorem sym2_image [DecidableEq β] (f : α → β) (s : Finset α) : (s.image f).sym2 = s.sym2.image (Sym2.map f) :=
by
apply val_injective
dsimp [Finset.sym2]
rw [← Multiset.dedup_sym2, Multiset.sym2_map]