comp_hasLimit

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Initial.comp_hasLimit

English

If there is a limit for F ⋙ G, then G has a limit.

Русский

Если существует предел для F ⋙ G, то у G существует предел.

LaTeX

$$$\\text{HasLimit}(F \\circ G) \\Rightarrow \\text{HasLimit}(G).$$$

Lean4

instance (priority := 100) comp_hasLimit [HasLimit G] : HasLimit (F ⋙ G) :=
  HasLimit.mk (limitConeComp F (getLimitCone G))

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

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

Разделы

Аффилиация

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