Theorems · Definition · combinatorics

monoEquivOfFin

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

Given a linearly ordered fintype α of cardinal k, the order isomorphism monoEquivOfFin α h is the increasing bijection between Fin k and α. Here, h is a proof that the cardinality of α is k. We use this instead of an isomorphism Fin (card α) ≃o α to avoid casting issues in further uses of this function.

Defined in

Mathlib.Data.Fintype.Sort

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeLinearOrder