exists_duplicate_iff_not_nodup

Mathlib.Data.List.Duplicate

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

English

There exists a duplicate in l if and only if l is not nodup.

Русский

Существует дубликат в l тогда и только тогда, когда l не имеет повторов.

LaTeX

$$$\exists x:\alpha, x \in+ l \quad\Longleftrightarrow\quad \neg Nodup(l)$$$

Lean4

theorem exists_duplicate_iff_not_nodup : (∃ x : α, x ∈+ l) ↔ ¬Nodup l := by simp [nodup_iff_forall_not_duplicate]

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

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

Разделы

Аффилиация

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