English
If α is a type with a unique element, then the map that sends a finite list to its length is a bijection between List α and ℕ, with inverse given by n ↦ replicate n default. In particular, List α ≃ ℕ.
Русский
Если у типа α есть уникальный элемент, то отображение, отправляющее конечный список в его длину, образует биекция между List α и ℕ; обратное отображение задано как n ↦ replicate n default. Таким образом, List α ≃ ℕ.
LaTeX
$$$\\forall \\alpha,\\ \\text{Unique }\\alpha\\implies \\text{List }\\alpha \\simeq \\mathbb{N},\\ \\text{toFun}=\\text{length},\\ \\text{invFun}(n)=\\text{List.replicate } n\\,\\text{default},\\ \\text{left_inv},\\ \\text{right_inv}. $$$
Lean4
/-- A list on a unique type is equivalent to ℕ by sending each list to its length. -/
@[simps!]
def listUniqueEquiv (α : Type*) [Unique α] : List α ≃ ℕ
where
toFun := List.length
invFun n := List.replicate n default
left_inv u := List.length_injective (by simp)
right_inv n := List.length_replicate
