uncurry_injective — Mathlib

English

Let A be exponentiable. The uncurry map uncurry : (Y ⟶ A ⟹ X) → (A ⊗ Y ⟶ X) is injective.

Русский

Пусть A экспоненцируемый, тогда отображение uncurry : (Y ⟶ A ⟹ X) → (A ⊗ Y ⟶ X) инъективно.

LaTeX

$$$\forall g,h:\; Y \to A \Rightarrow X,\; \operatorname{uncurry}(g) = \operatorname{uncurry}(h) \Rightarrow g=h$$$

Lean4

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

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