curry'_injective

Mathlib.CategoryTheory.Closed.Monoidal

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

English

Curry'_injective: if curry' f = curry' f' then f = f'.

Русский

Curry'_injective: если curry' f = curry' f', тогда f = f'.

LaTeX

$$$ \\forall {X Y} [Closed X],\\ {f f'}: X \\to Y,\\ curry' f = curry' f' \\Rightarrow f=f'. $$$

Lean4

theorem curry'_injective {X Y : C} [Closed X] {f f' : X ⟶ Y} (h : curry' f = curry' f') : f = f' :=
  curryHomEquiv'.injective h

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

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

Разделы

Аффилиация

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