mk_multiset_of_isEmpty

Mathlib.SetTheory.Cardinal.Finsupp

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_multiset_of_isEmpty

English

If α is empty, there is exactly one Multiset α, namely the empty multiset.

Русский

Если α пуст, существует ровно один мультисет α — пустой мультисет.

LaTeX

$$$$ \\#(\\mathrm{Multiset}\\; \\alpha) = 1. $$$$

Lean4

theorem mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : #(Multiset α) = 1 :=
  Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

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

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

Разделы

Аффилиация

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