instPreservesLimitsOfShapeπ₃

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃

English

For F: J ⥤ ShortComplex C with limits of π₁, π₂, π₃, π₃ preserves limits of shape J.

Русский

Для F: J ⥤ ShortComplex C с пределами π₁, π₂, π₃, π₃ сохраняет пределы формы J.

LaTeX

$$$ \text{PreservesLimitsOfShape } J \pi_3 $$$

Lean4

noncomputable instance : PreservesLimitsOfShape J (π₃ : _ ⥤ C) where

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

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

Разделы

Аффилиация

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