lift_π_app

Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.limit.lift_π_app

← MathLib Explorer

English

EssImage is closed under limits/colimits in basic settings

Русский

EssImage замкнуто по пределам/колимитам в базовых условиях

LaTeX

$$$\\text{essImage}$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_π_app (H : J ⥤ K ⥤ C) [HasLimit H] (c : Cone H) (j : J) (k : K) :
    (limit.lift H c).app k ≫ (limit.π H j).app k = (c.π.app j).app k :=
  congr_app (limit.lift_π c j) k

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

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

Разделы

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

Аффилиация

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