not_nodup_pair

Mathlib.Data.Multiset.AddSub

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

English

For any a, Nodup(a :: a :: 0) is false.

Русский

Для любого a мультимножество {a,a} не является Nodup.

LaTeX

$$$$ \neg \operatorname{Nodup}(a :: a :: 0) $$$$

Lean4

theorem not_nodup_pair : ∀ a : α, ¬Nodup (a ::ₘ a ::ₘ 0) :=
  List.not_nodup_pair

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

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

Разделы

Аффилиация

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