dedup_idem

Mathlib.Data.Multiset.Dedup

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

English

Applying dedup twice is the same as applying it once: dedup(dedup(m)) = dedup(m).

Русский

Повторное применение dedup не меняет результат: dedup(dedup(m)) = dedup(m).

LaTeX

$$$$dedup(dedup(m)) = dedup(m)$$$$

Lean4

@[simp]
theorem dedup_idem {m : Multiset α} : m.dedup.dedup = m.dedup :=
  Quot.induction_on m fun _ => @congr_arg _ _ _ _ ofList List.dedup_idem

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

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

Разделы

Аффилиация

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