instHasLimitsInd — Mathlib

English

If C has all limits, then Ind(C) has all limits. The Ind-construction preserves the existence of limits.

Русский

Если в C существуют все пределы, то и Ind(C) имеет все пределы. Конструкция Ind сохраняет существование пределов.

LaTeX

$$$\operatorname{HasLimits}(C) \Rightarrow \operatorname{HasLimits}(\mathrm{Ind}\,C)$$$

Lean4

instance [HasLimits C] : HasLimits (Ind C) :=
  hasLimits_of_hasLimits_createsLimits (Ind.inclusion C)

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