fromTypes_fin_const — Mathlib

English

There is a canonical equality between the type of functions Fin(n) → α with codomain β and the type of n-ary functions from α to β; i.e., FromTypes((Fin n) → α) β = OfArity α β n.

Русский

Существует каноническое равенство между множеством функций Fin(n) → α со значениями в β и множеством n-арных функций α^n → β; то есть FromTypes((Fin n) → α) β = OfArity α β n.

LaTeX

$$$\\mathrm{FromTypes}((\\mathrm{Fin}(n) \\to \\alpha))\\,\\beta = \\mathrm{OfArity}\\,\\alpha\\,\\beta\\,n$$$

Lean4

theorem fromTypes_fin_const (α β : Type u) (n : ℕ) : FromTypes (fun (_ : Fin n) => α) β = OfArity α β n :=
  rfl

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