fromTypes_fin_const_equiv — Mathlib

English

There is a definitional equivalence between heterogeneous functions with a fixed domain and n-ary functions with that domain; i.e., FromTypes((Fin n) → α) β ≃ OfArity α β n.

Русский

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

LaTeX

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

Lean4

/-- The definitional equality between heterogeneous functions with constant
domain and `n`-ary functions with that domain. -/
def fromTypes_fin_const_equiv (α β : Type u) (n : ℕ) : FromTypes (fun (_ : Fin n) => α) β ≃ OfArity α β n :=
  .refl _

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