Theorems · Definition · order theory

Fintype.orderIsoFinOfCardEq

(α : Type u_1) → [inst : LinearOrder α] → [inst_1 : Fintype α] → {k : ℕ} → Fintype.card α = k → Fin k ≃o α

Given a Fintype α of cardinality k, the map orderIsoFinOfCardEq s h is the increasing bijection between Fin k and α as an OrderIso. Here, h is a proof that the cardinality of α is k. We use this instead of an iso Fin (Fintype.card α) ≃o α to avoid casting issues in further uses of this function.

Defined in

Mathlib.Data.Finset.Sort

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderFintype