instFaithfulProdUncurry

Mathlib.CategoryTheory.Functor.Currying

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instFaithfulProdUncurry

English

Let C, D, E be categories. The uncurrying functor from Fun(C, Fun(D, E)) to Fun(C × D, E) is faithful.

Русский

Пусть C, D, E — категории. Функтор раскурривания из Fun(C, Fun(D, E)) в Fun(C × D, E) является верным.

LaTeX

$$$\operatorname{Faithful}(\operatorname{uncurry})$$$

Lean4

instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful :=
  fullyFaithfulUncurry.faithful

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

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

Разделы

Аффилиация

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