Theorems · Definition · order theory

Finset.orderIsoOfFin

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

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

Defined in

Mathlib.Data.Finset.Sort

Cited by

7 results in Mathlib

Foundations

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

Assumes

LinearOrder