uncurry_curry — Mathlib

English

For any X, uncurry of the identity on (A ⟹ X) equals the evaluation map ev_A at X: uncurry id = ev_A.app X.

Русский

Для любого X развёртывание тождественного морфизма на (A ⟹ X) равно оценке: uncurry id = ev_A.app X.

LaTeX

$$$\mathrm{uncurry} (\mathrm{Id}_{A \Rightarrow X}) = (\mathrm{ev}\, A).app X$$$

Lean4

@[simp]
theorem uncurry_curry (f : A ⊗ X ⟶ Y) : uncurry (curry f) = f :=
  (Closed.adj.homEquiv _ _).left_inv f

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