curry_injective — Mathlib

English

The curry operation is injective; knowing the curried form determines the original tensor-map uniquely.

Русский

Операция каррирования инъективна: знание карри-образа полностью определяет исходное отображение на тензорном произведении.

LaTeX

$$$\\text{curry} : (M \\otimes_R N \\to P) \\to M \\to_R N \\to_R P$ is injective, i.e. if $\\text{curry}(f)=\\text{curry}(g)$ then $f=g$.$$

Lean4

theorem curry_injective : Function.Injective (curry : (M ⊗[R] N →ₗ[R] P) → M →ₗ[R] N →ₗ[R] P) := fun _ _ H => ext H

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