sym2_image — Mathlib

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]

Похожие утверждения