Theorems · Definition · order theory

Finset.orderEmbOfFin

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

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

Defined in

Mathlib.Data.Finset.Sort

Cited by

47 results in Mathlib

Foundations

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

Assumes

LinearOrder