hasLimit — Mathlib

English

If the forgetful sections are small, F has a limit in GrpCat.

Русский

Если секции забывания малы, то F имеет предел в GrpCat.

LaTeX

$$$\\text{HasLimit } F$$$

Lean4

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

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