Theorems · Definition · combinatorics

Fintype.truncFinBijection

(α : Type u_4) → [inst : Fintype α] → Trunc { f // Function.Bijective f }

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 α].

Defined in

Mathlib.Data.Fintype.EquivFin

Cited by

0 results in Mathlib

Foundations

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

Assumes

Fintype