hasLimits — Mathlib

English

If T has limits, then the arrow category Arrow T also has limits of shape J for any J.

Русский

Если в категории T существуют пределы, то и категория стрел Arrow T имеет пределы формы J для любого J.

LaTeX

$$$\\operatorname{HasLimits}(T) \\Rightarrow \\operatorname{HasLimits}(\\mathrm{Arrow}(T))$$$

Lean4

instance hasLimits [HasLimits T] : HasLimits (Arrow T) :=
  ⟨fun _ _ => inferInstance⟩

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