forget₂AddCommMon_preservesLimits

English

The forgetful functor forget₂ from SemiRingCat to AddCommMonCat preserves limits of size.

Русский

Забывающий функтор forget₂: SemiRingCat → AddCommMonCat сохраняет пределы по размеру.

LaTeX

$$$\operatorname{PreservesLimitsOfSize}\big(\operatorname{forget}_2\, SemiRingCat\, AddCommMonCat\big)$$$

Lean4

instance forget₂AddCommMon_preservesLimits : PreservesLimits (forget₂ SemiRingCat AddCommMonCat.{u}) :=
  SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize.{u, u}

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