notMem_nil

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.notMem_nil

English

No element belongs to the unique element of Sym α 0.

Русский

Любой элемент не принадлежит единственному элементу Sym α 0.

LaTeX

$$$ \forall a:\alpha, a \notin (\mathrm{nil} : \mathrm{Sym}(\alpha,0)) $$$

Lean4

@[simp]
theorem notMem_nil (a : α) : a ∉ (nil : Sym α 0) :=
  Multiset.notMem_zero a

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

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

Разделы

Аффилиация

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