not_nodup_pair

Mathlib.Data.List.Nodup

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

English

The list [a, a] is not nodup.

Русский

Список [a, a] содержит дубликаты и не является нодуп.

LaTeX

$$$ \neg \operatorname{Nodup}([a,a]) $$$

Lean4

theorem not_nodup_pair (a : α) : ¬Nodup [a, a] :=
  not_nodup_cons_of_mem <| mem_singleton_self _

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

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

Разделы

Аффилиация

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