uncurry — Mathlib

English

The evaluation map at an object X is natural in X with respect to morphisms; i.e., for morphisms f: X → X', the induced maps commute with evaluation.

Русский

Оценочная карта в X естественна по отношению к отображениям; т. е. диаграмма естественности для оценок

LaTeX

$$$\mathrm{ev}_{X} \circ (f \otimes \mathrm{id}) = f \circ \mathrm{ev}_{X'}$$$

Lean4

/-- Uncurrying in a Cartesian-closed category. -/
def uncurry : (Y ⟶ A ⟹ X) → (A ⊗ Y ⟶ X) :=
  ((exp.adjunction A).homEquiv _ _).symm

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