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:
mono_equiv_of_fin: Order isomorphism between
fin (card α).
fin_sum_equiv_of_finset: Equivalence between
fin m ⊕ fin nwhere
nare respectively the cardinalities of some
finset αand its complement.
Given a linearly ordered fintype
α of cardinal
k, the order isomorphism
mono_equiv_of_fin α h is the increasing bijection between
fin k and
h is a proof
that the cardinality of
k. We use this instead of an isomorphism
fin (card α) ≃o α to
avoid casting issues in further uses of this function.
α is a linearly ordered fintype,
s : finset α has cardinality
m and its complement has
fin m ⊕ fin n ≃ α. The equivalence sends elements of
fin m to
s and elements of
fin n to elements of
sᶜ while preserving order on each
fin m ⊕ fin n (using
- fin_sum_equiv_of_finset hm hn = ((s.order_iso_of_fin hm).to_equiv.sum_congr ((sᶜ.order_iso_of_fin hn).to_equiv.trans (equiv.set.of_eq fin_sum_equiv_of_finset._proof_1))).trans (equiv.set.sum_compl ↑s (λ (a : α), finset.decidable_mem' a s))