English
The sym2 of the image under f equals the image under Sym2.map of s.sym2.
Русский
Sym2 образа под действием f равен образу Sym2.map f над s.sym2.
LaTeX
$$$ (f '' s).\mathrm{sym2} = \mathrm{Sym2.map} f '' s.\mathrm{sym2} $$$
Lean4
theorem sym2_image {f : α → β} {s : Set α} : (f '' s).sym2 = Sym2.map f '' s.sym2 :=
preimage_injective.mpr Sym2.mk_surjective <| by
simp_rw [sym2_eq_mk_image, prod_image_image_eq, image_image, Sym2.map_mk, Prod.map]