instIsEmptyToTypeOfNat

Mathlib.Data.Multiset.Fintype

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

English

The zero multiset is empty; i.e., 0 : Multiset α has no elements.

Русский

Нулевое мультимножество пусто; то есть 0 : Multiset α содержит ни одного элемента.

LaTeX

$$$ \text{IsEmpty}(0 : \mathrm{Multiset}\, \alpha) $$$

Lean4

instance : IsEmpty (0 : Multiset α) :=
  Fintype.card_eq_zero_iff.mp (by simp)

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

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

Разделы

Аффилиация

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