Let $X$ be a set of cardinality $n\in\N$ and $0\leq k\leq n$. A $k$-combination of $X$ is a $k$-sized subset of $X$.
For any $n$, $k\in\N$ with $k\leq n$, we define
\[C(n,k) = \big\lvert\powerset_k(\llbra n\rrbra)\big\rvert\]as the number of $k$-combinations of $\llbra n\rrbra$. It can then be shown that this is the number of $k$-combinations of any set of cardinality $n$.
$C(n,k)$ is also written as
\[\binom{n}{k},\]called the binomial coefficient.
Arranging the values of $C(n,k)$ into a triangular array gives Pascalβs Triangle:
\[\begin{gather*} 1 \\ 1 \quad 1 \\ 1 \quad 2 \quad 1 \\ 1 \quad 3 \quad 3 \quad 1 \\ 1 \quad 4 \quad 6 \quad 4 \quad 1 \\ 1 \quad 5 \quad 10 \quad 10 \quad 5 \quad 1 \\ \vdots \end{gather*}\]
For any $n$, $k\in\N$ with $k\leq n$,
\[C(n,k) = \frac{n!}{k!(n-k)!}.\]
Proof.The function
\[\varphi : \inj(\llbra k\rrbra,\llbra n\rrbra)\to\powerset_k(\llbra n\rrbra), \, f\mapsto\ran f\]is surjective. It is easy to see that for every $A\in\powerset_k(\llbra n\rrbra)$,
\[\big\lvert\varphi^{-1}[\{A\}]\big\rvert = \big\lvert\bij(\llbra k\rrbra,\llbra k\rrbra)\big\rvert.\]By PROP-PERM-BIJ,
\[\big\lvert\bij(\llbra k\rrbra,\llbra k\rrbra)\big\rvert = k!.\]So by PROP-CV-FC-C,
\[P(n,k) = k!\cdot C(n,k),\]whence
\[C(n,k) = \frac{P(n,k)}{k!} = \frac{n!}{k!(n-k)!}.\]β
For any $n\geq 2$ and $1\leq k\leq n-1$,
\[C(n,k) = C(n-1,k)+C(n-1,k-1).\]
Proof.For every $A\in\powerset_k(\llbra n\rrbra)$, either $n\in A$ or $n\notin A$. Hence
\[\powerset_k(\llbra n\rrbra) = \powerset_k(\llbra n-1\rrbra)\sqcup T,\]where
\[T = \big\{B\cup\{n\} : B\in\powerset_{k-1}(\llbra n-1\rrbra)\big\} \equ \powerset_{k-1}(\llbra n-1\rrbra).\]β
For any $n$, $k\in\N$ with $k\leq n$,
\[C(n,k) = C(n,n-k).\]
Proof.The function
\[\varphi : \powerset_k(\llbra n\rrbra)\to\powerset_{n-k}(\llbra n\rrbra), \, A\mapsto\llbra n\rrbra\setminus A\]is bijective.
For any $n\in\N$,
\[\sum_{k=0}^n C(n,k) = 2^n.\]
Proof.
\[\bigsqcup_{k=0}^n\powerset_k(\llbra n\rrbra) = \powerset(\llbra n\rrbra).\]By PROP-P-CARD,
\[\lvert\powerset(\llbra n\rrbra)\rvert = 2^n.\]β