dedup_cons

Mathlib.Data.Multiset.FinsetOps

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

English

Deduplicating a cons equals ndinsert of the head into dedup of the tail.

Русский

Удаление повторов у конструкторской пары даёт ndinsert головы в dedup хвоста.

LaTeX

$$$ \\text{dedup}(a ::\\! s) = \\mathrm{ndinsert}(a) (\\text{dedup } s) $$$

Lean4

theorem dedup_cons {a : α} {s : Multiset α} : dedup (a ::ₘ s) = ndinsert a (dedup s) := by
  by_cases h : a ∈ s <;> simp [h]

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

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

Разделы

Аффилиация

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