limitConeIsLimit — Mathlib

English

The limit cone for a diagram into RingCat is a limit cone; the chosen limit is universal.

Русский

Предел конуса диаграммы в RingCat является пределом; выбранный предел универсален.

LaTeX

$$$ \\operatorname{IsLimit}( \\text{limitCone } F )$$$

Lean4

/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
-/
def limitConeIsLimit : IsLimit (limitCone F) :=
  liftedLimitIsLimit _

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