instHasFiniteLimits

Mathlib.Algebra.Homology.HomologicalComplexLimits

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

English

If C has finite limits, then HomologicalComplex C c has finite limits.

Русский

Если у C есть конечные пределы, то у HomologicalComplex C c есть конечные пределы.

LaTeX

$$$ \text{HasFiniteLimits}(C) \Rightarrow \text{HasFiniteLimits}(\mathrm{HomologicalComplex}(C,c)).$$$

Lean4

instance [HasFiniteLimits C] : HasFiniteLimits (HomologicalComplex C c) :=
  ⟨fun _ _ => inferInstance⟩

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

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

Разделы

Аффилиация

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