English
If f is a order-embedding with image in s, then f equals the standard order embedding s.orderEmbOfFin h.
Русский
Если f — order-embedding с образом в s, то f равняется стандартному embeddings s.orderEmbOfFin h.
LaTeX
$$f = s.orderEmbOfFin h$$
Lean4
/-- Given a `Fintype` `α` of cardinality `k`, the map `orderIsoFinOfCardEq s h` is the increasing
bijection between `Fin k` and `α` as an `OrderIso`. Here, `h` is a proof that the cardinality of `α`
is `k`. We use this instead of an iso `Fin (Fintype.card α) ≃o α` to avoid casting issues in further
uses of this function. -/
def orderIsoFinOfCardEq (α : Type*) [LinearOrder α] [Fintype α] {k : ℕ} (h : Fintype.card α = k) : Fin k ≃o α :=
(Finset.univ.orderIsoOfFin h).trans ((OrderIso.setCongr _ _ Finset.coe_univ).trans OrderIso.Set.univ)
