English
For a Finset s with card k, there exists an order isomorphism between Fin k and s.
Русский
Пусть Finset s имеет кардинал k; между Fin k и s существует упорядоченное изоморфизм.
LaTeX
$$$ \\exists k\\ (s.\\operatorname{card} = k) \\;\\land\\; Fin k \\cong_o s $$$
Lean4
/-- Given a finset `s` of cardinality `k` in a linear order `α`, the map `orderIsoOfFin s h`
is the increasing bijection between `Fin k` and `s` as an `OrderIso`. Here, `h` is a proof that
the cardinality of `s` is `k`. We use this instead of an iso `Fin s.card ≃o s` to avoid
casting issues in further uses of this function. -/
def orderIsoOfFin (s : Finset α) {k : ℕ} (h : s.card = k) : Fin k ≃o s :=
OrderIso.trans (Fin.castOrderIso ((length_sort (α := α) (· ≤ ·)).trans h).symm) <|
(s.sort_sorted_lt.getIso _).trans <| OrderIso.setCongr _ _ <| Set.ext fun _ => mem_sort _
