instHasLimitsOfSizeModuleCat — Mathlib

English

The instance HasLimitsOfSize for ModuleCat R holds, i.e., ModuleCat R has limits of all small/relative sizes.

Русский

Существование пределов заданного размера в ModuleCat R: у ModuleCat R есть пределы всех малых размеров.

LaTeX

$$$\\mathrm{HasLimitsOfSize}(\\mathrm{ModuleCat}\\ R)$$$

Lean4

instance : HasLimitsOfSize.{u, u + 1} (ModuleCat.{u + 1} R) :=
  hasLimitsOfSizeShrink.{u, u + 1, u + 1, u + 1} _

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