singleton_ne_zero

Mathlib.Data.Multiset.ZeroCons

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

English

A singleton multiset {a} is never the empty multiset.

Русский

Мультимножество вида {a} никогда не является пустым.

LaTeX

$$$\{a\} \neq 0$$$

Lean4

@[simp]
theorem singleton_ne_zero (a : α) : ({ a } : Multiset α) ≠ 0 :=
  ne_of_gt (lt_cons_self _ _)

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

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

Разделы

Аффилиация

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