equivSigmaTuple — Mathlib

English

There is a natural bijection between lists and sigma-type tuples: List α ≃ Σ n, Fin n → α.

Русский

Существует естественное биективное соответствие между списками и сигма-типами: List α ≃ Σ n, Fin n → α.

LaTeX

$$$ \\operatorname{List} \\alpha \\simeq \\Sigma n,\\, \\mathrm{Fin} \\, n \\to \\alpha $$$

Lean4

/-- Lists are equivalent to the sigma type of tuples of a given length. -/
@[simps]
def equivSigmaTuple : List α ≃ Σ n, Fin n → α
    where
  toFun l := ⟨l.length, l.get⟩
  invFun f := List.ofFn f.2
  left_inv := List.ofFn_get
  right_inv := fun ⟨_, f⟩ => Fin.sigma_eq_of_eq_comp_cast length_ofFn <| funext fun i => get_ofFn f i

Похожие утверждения