nodup_iff_forall_not_duplicate

Mathlib.Data.List.Duplicate

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

English

A list is nodup if and only if no element is duplicated in it.

Русский

Список без повторов тогда, когда ни один элемент не дублируется в нем.

LaTeX

$$$Nodup(l) \iff \forall x:\alpha, \neg (x \in+ l)$$$

Lean4

theorem nodup_iff_forall_not_duplicate : Nodup l ↔ ∀ x : α, ¬x ∈+ l := by
  simp_rw [nodup_iff_sublist, duplicate_iff_sublist]

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

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

Разделы

Аффилиация

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