curryHomEquiv' — Mathlib

English

Uncurry' is injective: if uncurry' f = uncurry' f' then f = f'.

Русский

Uncurry' инъективен: если uncurry' f = uncurry' f' тогда f=f'.

LaTeX

$$$ \\forall {X} [Closed X], {f,f'}: 𝟙_C ⟶ (\\mathrm{ihom} X).obj Y,\\ uncurry' f = uncurry' f' \\Rightarrow f=f'. $$$

Lean4

/-- The bijection `(X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y)` in a monoidal closed category. -/
@[simps]
def curryHomEquiv' {X Y : C} [Closed X] : (X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y)
    where
  toFun := curry'
  invFun := uncurry'
  left_inv _ := by simp
  right_inv _ := by simp

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