English
If l has no duplicates, the get function induces a bijection between Fin(length l) and the set {x | x ∈ l}.
Русский
Если в списке l нет повторов, функция get дает биекцию между Fin(|l|) и множеством {x | x ∈ l}.
LaTeX
$$$ \\text{For a nodup } l:\\ \\mathrm{Fin}(\\mathrm{length}\\ l) \\cong\\ {x:\\alpha\\mid x\\in l}. $$$
Lean4
/-- If `l` has no duplicates, then `List.get` defines an equivalence between `Fin (length l)` and
the set of elements of `l`. -/
@[simps]
def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l }
where
toFun i := ⟨get l i, get_mem _ _⟩
invFun x := ⟨idxOf (↑x) l, idxOf_lt_length_iff.2 x.2⟩
left_inv i := by simp only [List.get_idxOf, Fin.eta, H]
right_inv x := by simp
