isLimit

Mathlib.CategoryTheory.Limits.Elements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CategoryOfElements.CreatesLimitsAux.isLimit

Lean4

/-- (implementation) The constructed limit cone is a limit cone. -/
noncomputable def isLimit : IsLimit (liftedCone F)
    where
  lift s := ⟨limit.lift (F ⋙ π A) ((π A).mapCone s), by simp⟩
  uniq s m h := ext _ _ _ <| limit.hom_ext fun i => by simpa using congrArg Subtype.val (h i)

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

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

Разделы

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

Аффилиация

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