not_nodup_cons_of_mem

Mathlib.Data.List.Nodup

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

English

If a ∈ l, then (a :: l) is not nodup.

Русский

Если a ∈ l, то a :: l содержит повторяющиеся элементы.

LaTeX

$$$ a \in l \rightarrow \neg (a::l).Nodup $$$

Lean4

theorem not_nodup_cons_of_mem : a ∈ l → ¬Nodup (a :: l) :=
  imp_not_comm.1 Nodup.notMem

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

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

Разделы

Аффилиация

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