uncurry'_injective

Mathlib.CategoryTheory.Closed.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalClosed.uncurry'_injective

← MathLib Explorer

English

Uncurry'_injective: if uncurry' f = uncurry' f' then f = f'.

Русский

Uncurry'_injective: если 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

theorem uncurry'_injective {X Y : C} [Closed X] {f f' : 𝟙_ C ⟶ (ihom X).obj Y} (h : uncurry' f = uncurry' f') :
    f = f' :=
  curryHomEquiv'.symm.injective h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru