mathlib documentation

data.fintype.sort

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 s is k. We use this instead of an isomorphism fin s.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 α} [decidable_pred s] (hm : s.card = m) (hn : s.card = n) :
fin m fin n α

If α is a linearly ordered type, 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 α} [decidable_pred s] (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 α} [decidable_pred s] (hm : s.card = m) (hn : s.card = n) (i : fin n) :