Cardinality_of_Set_of_Injections

Proved

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

cardinalitycardinality-of-set-of-injectionscombinatoricscounting-argumentsinjectionsproofwiki

Let $S$ and $T$ be finite sets. The number of injections from $S$ to $T$ , where $\card S = m, \card T = n$ is often denoted ${}^m P_n$ , and is ${}^m P_n = \begin{cases} \dfrac {n!} {\paren {n - m}!} & : m \le n \\ 0 & : m > n \end{cases}$

Preamble

import Mathlib.Data.Fintype.Card
import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Cardinality_of_Set_of_Injections (m n : ℕ) (hmn : m ≤ n) : Fintype.card {f : Fin m → Fin n // Function.Injective f} = Nat.factorial n / Nat.factorial (n - m) := by sorry

Source

https://proofwiki.org/wiki/Cardinality_of_Set_of_Injections

View graph