limitConeIsLimit — Mathlib

English

The equality between chosen limit cone is equal to the lifted limit; the constructed limit cone is a limit.

Русский

Существует равенство между выбранным пределом и поднятым пределом; конструкция предела действительно предел.

LaTeX

$$$ \text{limitConeIsLimit } F = \text{liftedLimitIsLimit}(\text{limit.isLimit}(F)) $$$

Lean4

/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.) -/
@[to_additive /-- The chosen cone is a limit cone.
    (Generally, you'll just want to use `limit.cone F`.) -/
    ]
noncomputable def limitConeIsLimit : IsLimit (limitCone.{v, u} F) :=
  liftedLimitIsLimit _

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