coneCompEval

Mathlib.CategoryTheory.Limits.Pi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.pi.coneCompEval

Lean4

/-- A cone over `F : J ⥤ Π i, C i` has as its components cones over each of the `F ⋙ Pi.eval C i`.
-/
def coneCompEval (c : Cone F) (i : I) : Cone (F ⋙ Pi.eval C i)
    where
  pt := c.pt i
  π :=
    { app := fun j => c.π.app j i
      naturality := fun _ _ f => congr_fun (c.π.naturality f) i }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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