limitConeIsLimit — Mathlib

English

Proof that the forgetful functor preserves or reflects limit structure via the constructed limit cone.

Русский

Доказательство того, что забывающий функтор сохраняет/отражает предел через сконструированный конус предела.

LaTeX

$$$\\text{IsLimit}(\\text{limitCone } 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 F) :=
  liftedLimitIsLimit _

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