isLimitToOver

Mathlib.CategoryTheory.Limits.Over

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.limit.isLimitToOver

Lean4

/-- If `F` has a limit, then the cone `limit.toUnder F` with cone point `𝟙 (limit F)` is
    also a limit cone. -/
def _root_.CategoryTheory.Limits.limit.isLimitToOver (F : J ⥤ C) [HasLimit F] : IsLimit (limit.toUnder F) :=
  Under.isLimitToUnder (limit.isLimit F)

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

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

Разделы

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

Аффилиация

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