dedup_sym2

Mathlib.Data.Multiset.Sym

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

English

For any m, dedup of m.sym2 equals dedup of m, then take sym2.

Русский

Для любого m, dedup(m.sym2) = dedup(m).sym2.

LaTeX

$$$ \\operatorname{dedup}(m^{\\mathrm{sym2}}) = \\operatorname{dedup}(m)^{\\mathrm{sym2}} $$$

Lean4

theorem dedup_sym2 [DecidableEq α] (m : Multiset α) : m.sym2.dedup = m.dedup.sym2 :=
  m.inductionOn fun xs => by simp [List.dedup_sym2]

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

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

Разделы

Аффилиация

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