English
There are finitely many embeddings between finite types: the set of injections α ↪ β is a finite type when α, β are finite.
Русский
Существует конечное число вложений между конечными типами: множество вложений α ↪ β является конечным.
LaTeX
$$$\\text{Fintype }(\\alpha \\hookrightarrow \\beta) $ is finite when $\\alpha, \\beta$ are finite.$$
Lean4
/-- There are finitely many embeddings between finite types.
This instance used to be computable (using `DecidableEq` arguments), but
it makes things a lot harder to work with here.
-/
noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β] : Fintype (α ↪ β) := by
classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
