English
If α is finite with a linear order and |α| = k, there exists a order isomorphism Fin k ≃o α.
Русский
Если α конечно, упорядочен по линейному порядку и |α| = k, существует порядковый изоморфизм Fin k ≃o α.
LaTeX
$$$\text{Fin}\\ k \\cong_o α$$$
Lean4
/-- 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. -/
def monoEquivOfFin (α : Type*) [Fintype α] [LinearOrder α] {k : ℕ} (h : Fintype.card α = k) : Fin k ≃o α :=
(univ.orderIsoOfFin h).trans <| (OrderIso.setCongr _ _ coe_univ).trans OrderIso.Set.univ
