Sorting a finite type #
This file provides two equivalences for linearly ordered fintypes:
mono_equiv_of_fin: Order isomorphism betweenαandfin (card α).fin_sum_equiv_of_finset: Equivalence betweenαandfin m ⊕ fin nwheremandnare respectively the cardinalities of somefinset αand its complement.
def
mono_equiv_of_fin
(α : Type u_1)
[fintype α]
[linear_order α]
{k : ℕ}
(h : fintype.card α = k) :
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) :
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
- 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))
@[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) :
⇑(fin_sum_equiv_of_finset hm hn) (sum.inl i) = ⇑(s.order_emb_of_fin hm) i
@[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) :
⇑(fin_sum_equiv_of_finset hm hn) (sum.inr i) = ⇑(sᶜ.order_emb_of_fin hn) i