English
There is a computable bijection between Fin(card α) and α, up to truncation, i.e., the bijection is realized by a member of a truncation of bijections.
Русский
Существует вычислимая биекция между Fin(card α) и α, с учётом трюк-обёртки (truncation).
LaTeX
$$$\mathrm{Trunc}\bigl\{ f:\mathrm{Fin}(\mathrm{card}\,\alpha) \to \alpha\;\big|\; \mathrm{Bijective}(f)\bigr\}.$$$
Lean4
/-- There is (computably) a bijection between `Fin (card α)` and `α`.
Since it is not unique and depends on which permutation
of the universe list is used, the bijection is wrapped in `Trunc` to
preserve computability.
See `Fintype.truncEquivFin` for a version that gives an equivalence
given `[DecidableEq α]`.
-/
def truncFinBijection (α) [Fintype α] : Trunc { f : Fin (card α) → α // Bijective f } :=
by
unfold card Finset.card
refine
Quot.recOnSubsingleton (motive := fun s : Multiset α =>
(∀ x : α, x ∈ s) → s.Nodup → Trunc { f : Fin (Multiset.card s) → α // Bijective f }) univ.val
(fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getBijectionOfForallMemList _ h)) mem_univ_val univ.2
