English
Given a finite set s with card at least k, there is an order-embedding Fin k ↪o α whose image lies in s.
Русский
Пусть кардинал s не меньше k; тогда существует порядок-встраивание Fin k ↪o α, образ которого лежит в s.
LaTeX
$$def orderEmbOfCardLe (s : Finset α) {k : ℕ} (h : k ≤ s.card) : Fin k ↪o α :=$$
Lean4
/-- Given a finset `s` of size at least `k` in a linear order `α`, the map `orderEmbOfCardLe`
is an order embedding from `Fin k` to `α` whose image is contained in `s`. Specifically, it maps
`Fin k` to an initial segment of `s`. -/
def orderEmbOfCardLe (s : Finset α) {k : ℕ} (h : k ≤ s.card) : Fin k ↪o α :=
(Fin.castLEOrderEmb h).trans (s.orderEmbOfFin rfl)
