# mathlibdocumentation

data.fintype.sort

# Sorting a finite type #

This file provides two equivalences for linearly ordered fintypes:

• mono_equiv_of_fin: Order isomorphism between α and fin (card α).
• fin_sum_equiv_of_finset: Equivalence between α and fin m ⊕ fin n where m and n are respectively the cardinalities of some finset α and its complement.
def mono_equiv_of_fin (α : Type u_1) [fintype α] [linear_order α] {k : } (h : = 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 α is k. We use this instead of an isomorphism fin (card α) ≃o α to avoid casting issues in further uses of this function.

Equations
def fin_sum_equiv_of_finset {α : Type u_1} [decidable_eq α] [fintype α] [linear_order α] {m n : } {s : finset α} (hm : s.card = m) (hn : s.card = n) :
fin m fin n α

If α is a linearly ordered fintype, s : finset α has cardinality m and its complement has cardinality n, then fin m ⊕ fin n ≃ α. The equivalence sends elements of fin m to elements of s and elements of fin n to elements of sᶜ while preserving order on each "half" of fin m ⊕ fin n (using set.order_iso_of_fin).

Equations
@[simp]
theorem fin_sum_equiv_of_finset_inl {α : Type u_1} [decidable_eq α] [fintype α] [linear_order α] {m n : } {s : finset α} (hm : s.card = m) (hn : s.card = n) (i : fin m) :
hn) (sum.inl i) = (s.order_emb_of_fin hm) i
@[simp]
theorem fin_sum_equiv_of_finset_inr {α : Type u_1} [decidable_eq α] [fintype α] [linear_order α] {m n : } {s : finset α} (hm : s.card = m) (hn : s.card = n) (i : fin n) :