ThmDex – An index of mathematical definitions, results, and conjectures.

Result R1839 on D15: Set cardinality

Cardinality of power set of a finite set

Formulation 0

Let $X$ be a D17: Finite set such that

(i)	$\mathcal{P}(X)$ is the D80: Power set of $X$

Then \begin{equation} |\mathcal{P}(X)| = 2^{|X|} \end{equation}

Formulation 1

Let $X$ be a D11: Set such that

(i)	\begin{equation} N : = \|X\| < \infty \end{equation}
(ii)	$\mathcal{P}(X)$ is the D80: Power set of $X$

Then \begin{equation} |\mathcal{P}(X)| = 2^N \end{equation}

Formulation 2

Then \begin{equation} \# \{ E : E \subseteq X \} = 2^{|X|} \end{equation}

Subresults

▶	R4309: Number of N-ary relations on a finite cartesian product

Proofs

Proof 0

Let $X$ be a D17: Finite set such that

(i)	$\mathcal{P}(X)$ is the D80: Power set of $X$

Let $\mathcal{M} : = \{ 0, 1 \}^X$ denote the D68: Set of maps from $X$ to $\{ 0, 1 \}$. Result R1841: Indicator function operator is a bijection shows that \begin{equation} |\mathcal{P}(X)| = |\mathcal{M}| \end{equation} and result R4314: Number of boolean functions on a finite set shows that \begin{equation} |\mathcal{M}| = 2^{|X|} \end{equation} $\square$