not_nodup

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.Duplicate.not_nodup

English

If x duplicates l, then l is not nodup.

Русский

Если x дублирует l, то l не содержит повторов.

LaTeX

$$$ List.Duplicate x l \rightarrow \neg Nodup(l) $$$

Lean4

theorem not_nodup (h : x ∈+ l) : ¬Nodup l := fun H => nodup_iff_forall_not_duplicate.mp H _ h

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

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

Разделы

Аффилиация

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