hasLimitsOfShape — Mathlib

English

Let J be a small category. If A and B have all limits of shape J and R preserves limits of shape J, then the comma category Comma(L,R) has all limits of shape J.

Русский

Пусть J — малая категория. Если в A и B существуют пределы любой формы J и R сохраняет пределы формы J, то запятая-категория Comma(L,R) имеет пределы формы J.

LaTeX

$$$\\operatorname{HasLimitsOfShape}(J,A) \\land \\operatorname{HasLimitsOfShape}(J,B) \\land \\operatorname{PreservesLimitsOfShape}(J,R) \\Rightarrow \\operatorname{HasLimitsOfShape}(J, \\mathrm{Comma}(L,R))$$$

Lean4

instance hasLimitsOfShape [HasLimitsOfShape J A] [HasLimitsOfShape J B] [PreservesLimitsOfShape J R] :
    HasLimitsOfShape J (Comma L R) where

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