English
There is a constructive embedding of α into β when card α ≤ card β, represented as a truncation of embeddings.
Русский
Существуют конструктивные вложения α в β при условии card α ≤ card β, представленные через усечение эмбеддингов.
LaTeX
$$$\\text{truncOfCardLE}: (\\operatorname{card} \\alpha \\le \\operatorname{card} \\beta) \\to Trunc (\\alpha \\hookrightarrow \\beta)$$$
Lean4
/-- A constructive embedding of a fintype `α` in another fintype `β` when `card α ≤ card β`. -/
def truncOfCardLE [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (h : Fintype.card α ≤ Fintype.card β) :
Trunc (α ↪ β) :=
(Fintype.truncEquivFin α).bind fun ea =>
(Fintype.truncEquivFin β).map fun eb => ea.toEmbedding.trans ((Fin.castLEEmb h).trans eb.symm.toEmbedding)
