English
If l lists all elements of α without duplicates, and every element of α belongs to l, then Fin(length l) is equinumerous with α.
Русский
Если список l перечисляет все элементы множества α без повторов, и каждый элемент α принадлежит l, то Fin(|l|) эквивалентно по числу с α.
LaTeX
$$$ \\operatorname{Nodup}(l) \\land (\\forall x:\\ alpha, x \\in l) \\Rightarrow Fin(\\mathrm{length}\\ l) \\simeq α. $$$
Lean4
/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
an equivalence between `Fin l.length` and `α`.
See `List.Nodup.getBijectionOfForallMemList` for a version without
decidable equality. -/
@[simps]
def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : Fin l.length ≃ α
where
toFun i := l.get i
invFun a := ⟨_, idxOf_lt_length_iff.2 (h a)⟩
left_inv i := by simp [List.idxOf_getElem, nd]
right_inv a := by simp
