sym2_map

Mathlib.Data.Multiset.Sym

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

English

For any f, (m.map f).sym2 = m.sym2.map (Sym2.map f).

Русский

Для любой f: (m.map f).sym2 = m.sym2.map (Sym2.map f).

LaTeX

$$$ (m.map f).sym2 = m.sym2.map (Sym2.map f) $$$

Lean4

theorem sym2_map (f : α → β) (m : Multiset α) : (m.map f).sym2 = m.sym2.map (Sym2.map f) :=
  m.inductionOn fun xs => by simp [List.sym2_map]

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

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

Разделы

Аффилиация

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