limitConeIsLimit — Mathlib

English

The constructed limit cone is actually a limit of the diagram F.

Русский

Построенный предел действительно является пределом диаграммы F.

LaTeX

$$$\\text{limitConeIsLimit}(F) : \\mathrm{IsLimit}(\\mathrm{limitCone}(F))$$$

Lean4

/-- (internal implementation) the fact that the proposed limit cone is the limit -/
@[simps]
noncomputable def limitConeIsLimit : IsLimit (limitCone.{v, u} F)
    where
  lift s
    v :=
    equivShrink F.sections
      { val := fun j => s.π.app j v
        property := fun f => congr_fun (Cone.w s f) _ }
  uniq := fun _ _ w => by
    ext x j
    simpa using congr_fun (w j) x

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