card_powersetCard

Mathlib.Data.Finset.Powerset

URI: https://scilib.ai/kg/mathlib#Finset.card_powersetCard

← MathLib Explorer

English

The number of n-element subsets of s is choose(|s|, n).

Русский

Число подмножеств s размерности n равно C(|s|, n).

LaTeX

$$card (powersetCard n s) = Nat.choose (card s) n$$

Lean4

/-- **Formula for the Number of Combinations** -/
@[simp]
theorem card_powersetCard (n : ℕ) (s : Finset α) : card (powersetCard n s) = Nat.choose (card s) n :=
  (card_pmap _ _ _).trans (Multiset.card_powersetCard n s.1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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