mk_finset_of_fintype

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_finset_of_fintype

English

If α is finite, then the cardinality of the set of finite subsets Finset α equals 2 raised to the cardinality of α.

Русский

Пусть α конечен; кардинал множества конечных подмножеств Finset α равен 2^{|α|}.

LaTeX

$$$\#(\mathrm{Finset}\,\alpha) = 2^{\mathrm{card}(\alpha)}$$$

Lean4

theorem mk_finset_of_fintype [Fintype α] : #(Finset α) = 2 ^ Fintype.card α := by simp

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

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

Разделы

Аффилиация

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