sym2_map

Mathlib.Data.Finset.Sym

URI: https://scilib.ai/kg/mathlib#Finset.sym2_map

English

Mapping by an embedding f commutes with sym2: (s.map f).sym2 = s.sym2.map (Sym2.map f).

Русский

Отображение через вложение f гармонирует с sym2: (s.map f).sym2 = s.sym2.map (Sym2.map f).

LaTeX

$$$(s.map f)^{\!\text{sym2}} = s^{\!\text{sym2}}.map(\text{Sym2.map } f)$$$

Lean4

theorem sym2_map (f : α ↪ β) (s : Finset α) : (s.map f).sym2 = s.sym2.map (.sym2Map f) :=
  val_injective <| s.val.sym2_map _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru