instHasLimitDiscreteWalkingPairCompPairEval

Mathlib.Algebra.Homology.HomologicalComplexBiprod

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instHasLimitDiscreteWalkingPairCompPairEval

← MathLib Explorer

English

The limit exists for the evaluation diagram at each index.

Русский

Существуют пределы для диаграммы оценки на каждом индексе.

LaTeX

$$$\\text{HasLimit}((\\mathrm{pair}\\; K\\; L) \\cdot (\\mathrm{eval}\\; C\\; c\\; i))$$$

Lean4

instance (i : ι) : HasLimit ((pair K L) ⋙ (eval C c i)) :=
  by
  have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
  exact hasLimit_of_iso e.symm

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

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

Разделы

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

Аффилиация

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