instIsEmptyToTypeEmptyCollection

Mathlib.Data.Multiset.Fintype

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

English

The empty multiset’s associated ToType is empty; i.e., the empty collection corresponds to an empty type.

Русский

Связанный с пустым мультимножество тип пуст; то есть пустая коллекция эквивалентна пустому типу.

LaTeX

$$$ IsEmpty (\mathrm{Multiset}.\mathrm{ToType}\, 0) $$$

Lean4

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

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

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

Разделы

Аффилиация

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