Theorems · Definition · combinatorics

Fintype.truncEquivFin

(α : Type u_4) → [DecidableEq α] → [inst : Fintype α] → Trunc (α ≃ Fin (Fintype.card α))

There is (computably) an equivalence between α and Fin (card α). Since it is not unique and depends on which permutation of the universe list is used, the equivalence is wrapped in Trunc to preserve computability. See Fintype.equivFin for the noncomputable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for an equiv α ≃ Fin n given Fintype.card α = n. See Fintype.truncFinBijection for a version without [DecidableEq α].

Defined in

Mathlib.Data.Fintype.EquivFin

Cited by

1 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintype