Theorems · Definition · combinatorics

Fintype.truncEquivFinOfCardEq

{α : Type u_1} → [inst : Fintype α] → [DecidableEq α] → {n : ℕ} → Fintype.card α = n → Trunc (α ≃ Fin n)

If the cardinality of α is n, there is computably a bijection between α and Fin n. See Fintype.equivFinOfCardEq for the noncomputable definition, and Fintype.truncEquivFin and Fintype.equivFin for the bijection α ≃ Fin (card α).

Defined in

Mathlib.Data.Fintype.EquivFin

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq