eq_nil_of_card_zero

Mathlib.Data.Sym.Basic

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

English

For any s ∈ Sym α 0, s equals nil; there is a unique element in Sym α 0.

Русский

Для любого s ∈ Sym α 0, s = nil; существует единственный элемент в Sym α 0.

LaTeX

$$$ \forall s \in \mathrm{Sym}(\alpha,0),\; s = \mathrm{nil}. $$$

Lean4

theorem eq_nil_of_card_zero (s : Sym α 0) : s = nil :=
  Subtype.ext <| Multiset.card_eq_zero.1 s.2

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

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

Разделы

Аффилиация

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