nodup_dedup

Mathlib.Data.List.Dedup

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

English

For any list l, the deduplicated list has no repeated elements; i.e., it is Nodup.

Русский

Для любого списка l упрощённый список не содержит повторяющихся элементов; то есть он является словарём без повторов.

LaTeX

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

Lean4

theorem nodup_dedup : ∀ l : List α, Nodup (dedup l) :=
  pairwise_pwFilter

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

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

Разделы

Аффилиация

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