forget₂CommSemiRing_preservesLimits

English

The forgetful functor forget₂ CommRingCat CommSemiRingCat preserves limits of size.

Русский

Забывающий функтор CommRingCat → CommSemiRingCat сохраняет пределы размера.

LaTeX

$$$\mathrm{forget}_2\text{CommRingCat_preservesLimitsOfSize}$$$

Lean4

instance forget₂CommSemiRing_preservesLimits : PreservesLimits (forget₂ CommRingCat CommSemiRingCat.{u}) :=
  CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize.{u, u}

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