sym2_image — Mathlib

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]

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