instFinalProdProd'

Mathlib.CategoryTheory.Limits.Sifted

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instFinalProdProd'

English

If F and G are final functors, then their product F.prod' G is a final functor.

Русский

Если F и G — финальные функторы, то их произведение F.prod' G является финальным функтором.

LaTeX

$$If F: C ⥤ D and G: C ⥤ D', with F, G final, then (F.prod' G).Final$$

Lean4

instance [F.Final] [G.Final] : (F.prod' G).Final :=
  show (diag C ⋙ F.prod G).Final from final_comp _ _

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

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

Разделы

Аффилиация

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