Documentation

Mathlib.Data.Fintype.Sort

Sorting a finite type #

This file provides two equivalences for linearly ordered fintypes:

def monoEquivOfFin (α : Type u_1) [inst : Fintype α] [inst : 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.

Equations
def finSumEquivOfFinset {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] [inst : LinearOrder α] {m : } {n : } {s : Finset α} (hm : Finset.card s = m) (hn : Finset.card (s) = 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 mto elements ofsand elements ofFin nto elements ofsᶜwhile preserving order on each "half" ofFin m ⊕ Fin n(usingSet.orderIsoOfFin`).

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem finSumEquivOfFinset_inl {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] [inst : LinearOrder α] {m : } {n : } {s : Finset α} (hm : Finset.card s = m) (hn : Finset.card (s) = n) (i : Fin m) :
↑(finSumEquivOfFinset hm hn) (Sum.inl i) = (Finset.orderEmbOfFin s hm).toEmbedding i
@[simp]
theorem finSumEquivOfFinset_inr {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] [inst : LinearOrder α] {m : } {n : } {s : Finset α} (hm : Finset.card s = m) (hn : Finset.card (s) = n) (i : Fin n) :
↑(finSumEquivOfFinset hm hn) (Sum.inr i) = (Finset.orderEmbOfFin (s) hn).toEmbedding i