Sorting a finite type

This file provides two equivalences for linearly ordered fintypes:

• monoEquivOfFin: Order isomorphism between α and Fin (card α).
• finSumEquivOfFinset: Equivalence between α and Fin m ⊕ Fin n where m and n are respectively the cardinalities of some Finset α and its complement.

def monoEquivOfFin (α : Type u_1) [Fintype α] [LinearOrder α] {k : ℕ} (h : 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.

def finSumEquivOfFinset {α : Type u_1} [DecidableEq α] [Fintype α] [LinearOrder α] {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.orderIsoOfFin).

@[simp]

theorem finSumEquivOfFinset_inl {α : Type u_1} [DecidableEq α] [Fintype α] [LinearOrder α] {m n : ℕ} {s : Finset α} (hm : s.card = m) (hn : sᶜ.card = n) (i : Fin m) : (finSumEquivOfFinset hm hn) (Sum.inl i) = (s.orderEmbOfFin hm) i

@[simp]

theorem finSumEquivOfFinset_inr {α : Type u_1} [DecidableEq α] [Fintype α] [LinearOrder α] {m n : ℕ} {s : Finset α} (hm : s.card = m) (hn : sᶜ.card = n) (i : Fin n) : (finSumEquivOfFinset hm hn) (Sum.inr i) = (sᶜ.orderEmbOfFin hn) i