English
Given s and k, a unique order-embedding f : Fin k ↪o α with f x ∈ s is f = s.orderEmbOfFin h.
Русский
Если дано s и k, единственное отображение-врезка f: Fin k ↪o α с изображением в s равно s.orderEmbOfFin h.
LaTeX
$$f = s.orderEmbOfFin h$$
Lean4
/-- Two parametrizations `orderEmbOfFin` of the same set take the same value on `i` and `j` if
and only if `i = j`. Since they can be defined on a priori not defeq types `Fin k` and `Fin l`
(although necessarily `k = l`), the conclusion is rather written `(i : ℕ) = (j : ℕ)`. -/
@[simp]
theorem orderEmbOfFin_eq_orderEmbOfFin_iff {k l : ℕ} {s : Finset α} {i : Fin k} {j : Fin l} {h : s.card = k}
{h' : s.card = l} : s.orderEmbOfFin h i = s.orderEmbOfFin h' j ↔ (i : ℕ) = (j : ℕ) :=
by
substs k l
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff
