powersetCard_coe'

Mathlib.Data.Multiset.Powerset

URI: https://scilib.ai/kg/mathlib#Multiset.powersetCard_coe'

English

For any n and list l, powersetCard of the multiset of l equals powersetCardAux n l.

Русский

Для любого n и списка l powersetCard примет мультимножество l как powersetCardAux n l.

LaTeX

$$powersetCard(n, \\uparrow l) = powersetCardAux(n, l)$$

Lean4

theorem powersetCard_coe' (n) (l : List α) : @powersetCard α n l = powersetCardAux n l :=
  rfl

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

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

Разделы

Аффилиация

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