curry_two_eq_curry — Mathlib

English

For two-argument dependent type p, any function f on the pair (p 0, p 1) is equivalent to a curried function via the piFinTwoEquiv p.

Русский

Для зависимого типа из двух аргументов p существует эквиваленция между функцией на пару и каррированной функцией через piFinTwoEquiv p.

LaTeX

$$$\\forall p: Fin 2 \\to Type,\\ \\forall f:( (i:Fin 2) \\to p i)\\to \\tau,\\; curry f = \\text{Function.curry} (f \\circ (piFinTwoEquiv p)^{-1})$$$

Lean4

theorem curry_two_eq_curry {p : Fin 2 → Type u} {τ : Type u} (f : ((i : Fin 2) → p i) → τ) :
    curry f = Function.curry (f ∘ (piFinTwoEquiv p).symm) :=
  rfl

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