curry_eq_iff — Mathlib

English

Two morphisms correspond under curry-uncurry iff they are translates of each other by the adjunction.

Русский

Две морфизмы соответствуют друг другу через карри-uncurry если они связаны переходом по адъюнкции.

LaTeX

$$$\mathrm{curry} f = g \iff \mathrm{uncurry} g = f$$$

Lean4

theorem curry_eq_iff (f : A ⊗ Y ⟶ X) (g : Y ⟶ A ⟶[C] X) : curry f = g ↔ f = uncurry g :=
  Adjunction.homEquiv_apply_eq (ihom.adjunction A) f g

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