dedup_eq_self

Mathlib.Data.List.Dedup

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

English

Dedup(l) equals l if and only if l is nodup (has no duplicates).

Русский

Dedup(l) равен l тогда и только тогда, когда l не имеет повторов.

LaTeX

$$$\\mathrm{dedup}(l) = l \\;\\iff\\; \\mathrm{Nodup}(l)$$$

Lean4

theorem dedup_eq_self {l : List α} : dedup l = l ↔ Nodup l :=
  pwFilter_eq_self

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

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

Разделы

Аффилиация

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