English
If l is sorted, there exists an order isomorphism between Fin(length l) and the set of elements of l.
Русский
Если список отсортирован, существует отображение-изоморфизм порядка между Fin(|l|) и множеством элементов списка l.
LaTeX
$$$ \\exists H:\\,\\mathrm{Fin}(\\mathrm{length}\\ l) \\cong_o \\{ x\\mid x\\in l\\} \\text{ given } l \\text{ sorted}. $$$
Lean4
/-- If `l` is a list sorted w.r.t. `(<)`, then `List.get` defines an order isomorphism between
`Fin (length l)` and the set of elements of `l`. -/
def getIso (l : List α) (H : Sorted (· < ·) l) : Fin (length l) ≃o { x // x ∈ l }
where
toEquiv := H.nodup.getEquiv l
map_rel_iff' := H.get_strictMono.le_iff_le
