isLimitConeOfHasLimitCurryCompLim

English

The cone described for HasLimit CurryCompLim is a limit cone.

Русский

Указанный конус для HasLimit CurryCompLim является пределом.

LaTeX

$$$\text{IsLimit }(\text{coneOfHasLimitCurryCompLim } G)$.$$

Lean4

/-- The cone `coneOfHasLimitCurryCompLim` is in fact a limit cone.
-/
noncomputable def isLimitConeOfHasLimitCurryCompLim : IsLimit (coneOfHasLimitCurryCompLim G) :=
  let Q : DiagramOfCones (curry.obj G) := .mkOfHasLimits _
  let Q' : ∀ j, IsLimit (Q.obj j) := fun j => limit.isLimit _
  { lift c' := limit.lift (F := curry.obj G ⋙ lim) (coneOfConeCurry G Q' c')
    fac c' f := by simp [coneOfHasLimitCurryCompLim, Q, Q']
    uniq c' f
      h := by
      dsimp [coneOfHasLimitCurryCompLim] at f h ⊢
      refine limit.hom_ext (F := curry.obj G ⋙ lim) (fun j ↦ limit.hom_ext (fun k ↦ ?_))
      simp [h ⟨j, k⟩, Q'] }

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