equivFin — Mathlib

English

There is (noncomputable) an equivalence between α and Fin(card α).

Русский

Существует (невычислимое) эквиваленция между α и Fin(card α).

LaTeX

$$$\alpha \simeq \mathrm{Fin}(\mathrm{card}\,\alpha).$$$

Lean4

/-- There is (noncomputably) an equivalence between `α` and `Fin (card α)`.

See `Fintype.truncEquivFin` for the computable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq`
for an equiv `α ≃ Fin n` given `Fintype.card α = n`.
-/
noncomputable def equivFin (α) [Fintype α] : α ≃ Fin (card α) :=
  letI := Classical.decEq α
  (truncEquivFin α).out

Похожие утверждения