mathlib3 documentation

data.fintype.sort

Sorting a finite type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides two equivalences for linearly ordered fintypes:

def mono_equiv_of_fin (α : Type u_1) [fintype α] [linear_order α] {k : } (h : fintype.card α = 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) :
@[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) :