forget_createsLimitsOfSize — Mathlib

English

For the forgetful functor forget MonCat, there are limits of every size created by forgetful lifting.

Русский

Для забывающей функции forget MonCat существуют пределы любого размера, создаваемые поднимающим.

LaTeX

$$$\text{CreatesLimitsOfSize }(\text{forget MonCat})$$$

Lean4

/-- The forgetful functor from monoids to types preserves all limits. -/
@[to_additive /-- The forgetful functor from additive monoids to types preserves all limits. -/
    ]
noncomputable instance forget_createsLimitsOfSize : CreatesLimitsOfSize.{w, v} (forget MonCat.{u}) where
  CreatesLimitsOfShape := inferInstance

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