instCategoryComp

Mathlib.CategoryTheory.Pi.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pi.instCategoryComp

Lean4

instance (f : J → I) : (j : J) → Category ((C ∘ f) j) :=
  inferInstanceAs <| (j : J) → Category (C (f j))

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

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

Разделы

Аффилиация

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