zero_ne_singleton

Mathlib.Data.Multiset.ZeroCons

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

English

A singleton multiset is nonempty, i.e., 0 is not equal to {a}.

Русский

Одиночное мультимножество непусто, то есть 0 не равно {a}.

LaTeX

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

Lean4

@[simp]
theorem zero_ne_singleton (a : α) : 0 ≠ ({ a } : Multiset α) :=
  singleton_ne_zero _ |>.symm

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

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

Разделы

Аффилиация

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