card_powerset — Mathlib

English

For any finite set S, the number of subsets of S equals 2^{|S|}. Equivalently, the card of the powerset of S is 2^{card(S)}.

Русский

Для любого конечного множества S число подмножеств S равно 2^{|S|}. Иными словами, |P(S)| = 2^{|S|}.

LaTeX

$$$\operatorname{card}(\mathcal{P}(s)) = 2^{\operatorname{card}(s)}$$$

Lean4

/-- **Number of Subsets of a Set** -/
@[simp]
theorem card_powerset (s : Finset α) : card (powerset s) = 2 ^ card s :=
  (card_pmap _ _ _).trans (Multiset.card_powerset s.1)

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