card_powerset

Mathlib.Data.Multiset.Powerset

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

English

The number of submultisets of s equals 2 raised to the power of the number of elements in s.

Русский

Число подмультимножеств множества s равно 2^{|s|}.

LaTeX

$$$ \\operatorname{card}(\\mathrm{powerset}(s)) = 2^{\\operatorname{card}(s)} $$$

Lean4

@[simp]
theorem card_powerset (s : Multiset α) : card (powerset s) = 2 ^ card s :=
  Quotient.inductionOn s <| by simp

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

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

Разделы

Аффилиация

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