mathlib documentation

data.fintype.sort

def mono_equiv_of_fin (α : Type u_1) [fintype α] [linear_order α] {k : } :
fintype.card α = kfin k α

Given a linearly ordered fintype α of cardinal k, the equiv 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 a map fin s.card → α to avoid casting issues in further uses of this function.

Equations