mem_ndinsert

Mathlib.Data.Multiset.FinsetOps

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mem_ndinsert {a b : α} {s : Multiset α} : a ∈ ndinsert b s ↔ a = b ∨ a ∈ s :=
  Quot.inductionOn s fun _ => mem_insert_iff

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

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

Разделы

Аффилиация

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