card_finset

Mathlib.Data.Fintype.Powerset

URI: https://scilib.ai/kg/mathlib#Fintype.card_finset

English

For a finite α, the number of finite subsets equals 2^{|α|}.

Русский

Для конечного α число конечных подмножеств равно 2^{|α|}.

LaTeX

$$$|\\mathrm{Finset}(\\alpha)| = 2^{|\\alpha|}.$$$

Lean4

@[simp]
theorem card_finset [Fintype α] : Fintype.card (Finset α) = 2 ^ Fintype.card α :=
  Finset.card_powerset Finset.univ

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

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

Разделы

Аффилиация

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