card_set

Mathlib.Data.Fintype.Powerset

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

English

The cardinality of Set α is 2^{|α|}.

Русский

Кардинал множества Set α равен 2^{|α|}.

LaTeX

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

Lean4

@[simp]
theorem card_set [Fintype α] : Fintype.card (Set α) = 2 ^ Fintype.card α :=
  (Finset.card_map _).trans (Finset.card_powerset _)

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

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

Разделы

Аффилиация

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