# Sorting a finite type #

This file provides two equivalences for linearly ordered fintypes:

`monoEquivOfFin`

: Order isomorphism between`α`

and`Fin (card α)`

.`finSumEquivOfFinset`

: Equivalence between`α`

and`Fin m ⊕ Fin n`

where`m`

and`n`

are respectively the cardinalities of some`Finset α`

and its complement.

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

- monoEquivOfFin α h = OrderIso.trans (Finset.orderIsoOfFin Finset.univ h) (OrderIso.trans (OrderIso.setCongr (↑Finset.univ) Set.univ (_ : ↑Finset.univ = Set.univ)) OrderIso.Set.univ)

## Instances For

def
finSumEquivOfFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
[LinearOrder α]
{m : ℕ}
{n : ℕ}
{s : Finset α}
(hm : Finset.card s = m)
(hn : Finset.card sᶜ = 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.orderIsoOfFin`

).

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

@[simp]

theorem
finSumEquivOfFinset_inl
{α : Type u_1}
[DecidableEq α]
[Fintype α]
[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) i

@[simp]

theorem
finSumEquivOfFinset_inr
{α : Type u_1}
[DecidableEq α]
[Fintype α]
[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) i