powersetCardAux_nil

Mathlib.Data.Multiset.Powerset

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

English

For any n, powersetCardAux(n+1, ∅) = ∅.

Русский

Для любого n, powersetCardAux(n+1, ∅) = ∅.

LaTeX

$$powersetCardAux(n+1, \\emptyset) = []$$

Lean4

@[simp]
theorem powersetCardAux_nil (n : ℕ) : powersetCardAux (n + 1) (@nil α) = [] :=
  rfl

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

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

Разделы

Аффилиация

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