uncurry_eq

Mathlib.CategoryTheory.Closed.Cartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianClosed.uncurry_eq

English

For A, X, uncurry of identity on A ⟹ X equals ev_A.app X.

Русский

Для A и X, uncurry идентичности на A ⟹ X даёт ev_A.app X.

LaTeX

$$$\mathrm{uncurry}(\mathrm{Id}_{A \Rightarrow X}) = (\mathrm{ev}\, A).app X$$$

Lean4

theorem uncurry_eq (g : Y ⟶ A ⟹ X) : uncurry g = (A ◁ g) ≫ (exp.ev A).app X :=
  rfl

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

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

Разделы

Аффилиация

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