dedup_idem

Mathlib.Data.List.Dedup

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

English

Dedup is idempotent: dedup(dedup(l)) = dedup(l).

Русский

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

LaTeX

$$$\\mathrm{dedup}(\\mathrm{dedup}(l)) = \\mathrm{dedup}(l)$$$

Lean4

@[simp]
theorem dedup_idem {l : List α} : dedup (dedup l) = dedup l :=
  pwFilter_idem

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

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

Разделы

Аффилиация

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