uncurry_expComparison — Mathlib

English

The uncurrying operation commutes with the exponential comparison: uncurry of expComparison equals the composition of prod/exp constructions with F.

Русский

Развертывание и сравнение экспоненциальных отображений договариваются: uncurry expComparison равно композиции prod/exp через F.

LaTeX

$$$ \\text{uncurry}(\\mathrm{expComparison}(F,A)) = \\mathrm{inv}(\\mathrm{prodComparison}(F,A,\\mathrm{exp}(A))) \\circ F.map(\\mathrm{exp.ev}(A)).$$$

Lean4

theorem uncurry_expComparison (A B : C) :
    CartesianClosed.uncurry ((expComparison F A).natTrans.app B) =
      inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) :=
  by rw [uncurry_eq, expComparison_ev]

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