Cardinality_of_Set_of_Subsets

Proved

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

cardinality-of-set-of-subsetscombinationscombinatoricsproofwiki

Let $S$ be a set such that $\card S = n$ . Let $m \le n$ . Then the number of subsets $T$ of $S$ such that $\card T = m$ is ${}^m C_n = \dfrac {n!} {m! \paren {n - m}!}$

Preamble

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Cardinality_of_Set_of_Subsets (n m : ℕ) (hmn : m ≤ n) : Nat.choose n m = Nat.factorial n / (Nat.factorial m * Nat.factorial (n - m)) := by sorry

Source

https://proofwiki.org/wiki/Cardinality_of_Set_of_Subsets

View graph