curry_injective — Mathlib

English

Fix A,Y,X with A exponentiable. The curry operation is injective: the map curry : (A ⊗ Y ⟶ X) → (Y ⟶ A ⟹ X) is injective.

Русский

Зафиксируем A, Y, X с свойством экспоненциируемости A. Операция карри инъективна: отображение curry : (A ⊗ Y ⟶ X) → (Y ⟶ A ⟹ X) инъективно.

LaTeX

$$$\forall f,g:\; A \otimes Y \to X,\; \operatorname{curry}(f) = \operatorname{curry}(g) \Rightarrow f=g$$$

Lean4

theorem curry_injective : Function.Injective (curry : (A ⊗ Y ⟶ X) → (Y ⟶ A ⟹ X)) :=
  (Closed.adj.homEquiv _ _).injective

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