uncurry_two_eq_uncurry — Mathlib

English

Specializing to arity 2, uncurry on a 2-ary function equals the uncurry composed with the canonical isomorphism from the two-element index. It expresses a concrete instance of the general uncurry/curry compatibility.

Русский

Для арности 2 раскуривание функции равно раскуриванию после канонического изomорфизма двух позиций. Это частный случай совместимости карри/раскуривания.

LaTeX

$$$\forall f: \mathrm{OfArity}\; \alpha\; \beta\; 2,\quad \operatorname{uncurry} f = \operatorname{Function.uncurry} f \circ (\mathrm{finTwoArrowEquiv}\ \alpha)$$$

Lean4

theorem uncurry_two_eq_uncurry {α β : Type u} (f : OfArity α β 2) :
    uncurry f = Function.uncurry f ∘ (finTwoArrowEquiv α) :=
  FromTypes.uncurry_two_eq_uncurry _ _ f

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