uncurry'_curry'

Mathlib.CategoryTheory.Closed.Monoidal

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

← MathLib Explorer

English

Curry' is injective: if curry' f = curry' f' then f = f'.

Русский

Curry' инъективен: если 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

/-- `curry'` and `uncurry`' are inverse bijections. -/
@[simp]
theorem uncurry'_curry' {X Y : C} [Closed X] (f : X ⟶ Y) : uncurry' (curry' f) = f := by simp [curry', uncurry']

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

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

Разделы

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

Аффилиация

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