Cardinality_of_Power_Set_of_Finite_Set

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cardinalitycardinality-of-power-setcombinatoricspower-setproofwiki

Let $S$ be a set such that $\card S = n$ where $\card S$ denotes the cardinality of $S$ , Then $\card {\powerset S} = 2^n$ where $\powerset S$ denotes the power set of $S$ .

Preamble

import Mathlib.Data.Fintype.Powerset

Formal statement

theorem Cardinality_of_Power_Set_of_Finite_Set {S : Type _} [Fintype S] : Fintype.card (Set S) = 2 ^ Fintype.card S := by sorry

Source

https://proofwiki.org/wiki/Cardinality_of_Power_Set_of_Finite_Set

View graph