monoidalClosed_uncurry — Mathlib

English

Uncurrying is the inverse of curry: for f: N ⟶ M ⟶ P, the map uncurry f sends x ⊗ y to f y applied to x.

Русский

Раскуррирование — обратное карри: для f: N ⟶ M ⟶ P отображение uncurry f на x ⊗ y даёт f(y) применённое к x.

LaTeX

$$$\\mathrm{MonoidalClosed.uncurry}(f)(x \\otimes y) = (f(y)).hom(x)$$$

Lean4

@[simp]
theorem monoidalClosed_uncurry {M N P : ModuleCat.{u} R} (f : N ⟶ M ⟶[ModuleCat.{u} R] P) (x : M) (y : N) :
    MonoidalClosed.uncurry f (x ⊗ₜ[R] y) = (f y).hom x :=
  rfl

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