hasLimit — Mathlib

English

A repeated assertion that forget₂ creates a limit for a diagram into MonCat.

Русский

Повторное утверждение, что forget₂ создаёт предел для диаграммы в MonCat.

LaTeX

$$$\text{forget₂CreatesLimit } F$$$

Lean4

/-- If `(F ⋙ forget CommMonCat).sections` is `u`-small, `F` has a limit. -/
@[to_additive /-- If `(F ⋙ forget AddCommMonCat).sections` is `u`-small, `F` has a limit. -/
    ]
instance hasLimit : HasLimit F :=
  HasLimit.mk
    { cone := limitCone F
      isLimit := limitConeIsLimit F }

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