hasFiniteLimits

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.hasFiniteLimits

English

If C has finite limits, then ShortComplex C has finite limits.

Русский

Если в C существуют конечные пределы, то у ShortComplex C есть конечные пределы.

LaTeX

$$$ \text{HasFiniteLimits } C \Rightarrow \text{HasFiniteLimits } (\text{ShortComplex } C) $$$

Lean4

instance hasFiniteLimits : HasFiniteLimits (ShortComplex C) :=
  ⟨fun _ _ _ => inferInstance⟩

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

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

Разделы

Аффилиация

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