instFullProdUncurry

Mathlib.CategoryTheory.Functor.Currying

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

English

The instance that uncurry is full (hence fully faithful) as provided by the previous theorem.

Русский

Экземпляр, доказывающий полноту раскрещивания (то есть его полную верность) следует из предыдущей теоремы.

LaTeX

$$$ \text{uncurry}.Full $$$

Lean4

instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full :=
  fullyFaithfulUncurry.full

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

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

Разделы

Аффилиация

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