mathlib documentation


def mono_equiv_of_fin (α : Type u_1) [fintype α] [linear_order α] {k : } (h : fintype.card α = k) :
fin k ≃o α

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