English
There is an order embedding Fin k ↪o α for a Finset s of size k in α.
Русский
Существует вложение по порядку Fin k ↪o α для Finset s размером k в α.
LaTeX
$$$ Fin k \\hookrightarrow_o \\alpha $$$
Lean4
/-- Given a finset `s` of cardinality `k` in a linear order `α`, the map `orderEmbOfFin s h` is
the increasing bijection between `Fin k` and `s` as an order embedding into `α`. Here, `h` is a
proof that the cardinality of `s` is `k`. We use this instead of an embedding `Fin s.card ↪o α` to
avoid casting issues in further uses of this function. -/
def orderEmbOfFin (s : Finset α) {k : ℕ} (h : s.card = k) : Fin k ↪o α :=
(orderIsoOfFin s h).toOrderEmbedding.trans (OrderEmbedding.subtype _)
