mem_dedup

Mathlib.Data.Multiset.Dedup

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

English

An element lies in the deduplicated multiset iff it lies in the original multiset.

Русский

Элемент принадлежит dedup s тогда, когда он принадлежит s.

LaTeX

$$$a \in dedup s \iff a \in s$$$

Lean4

@[simp]
theorem mem_dedup {a : α} {s : Multiset α} : a ∈ dedup s ↔ a ∈ s :=
  Quot.induction_on s fun _ => List.mem_dedup

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

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

Разделы

Аффилиация

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