uncurry_id_eq_ev

Mathlib.CategoryTheory.Closed.Cartesian

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

English

For any A and X, uncurry of the identity on A ⟹ X equals the evaluation component ev_A at 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_id_eq_ev (A X : C) [Exponentiable A] : uncurry (𝟙 (A ⟹ X)) = (exp.ev A).app X := by
  rw [uncurry_eq, whiskerLeft_id_assoc]

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

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

Разделы

Аффилиация

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