def
mono_equiv_of_fin
(α : Type u_1)
[fintype α]
[decidable_linear_order α]
{k : ℕ} :
fintype.card α = k → fin 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.