limitUncurryIsoLimitCompLim_hom_π_π

English

coneOfConeUncurryIsLimit asserts that the cone built from a family of limit cones is itself a limit cone.

Русский

coneOfConeUncurryIsLimit утверждает, что конус, построенный из семейства предельных конусов, сам является пределом.

LaTeX

$$$\text{coneOfConeUncurryIsLimit } Q c: IsLimit\; (\text{coneOfConeUncurry } Q c).$$$

Lean4

@[simp, reassoc]
theorem limitUncurryIsoLimitCompLim_hom_π_π {j} {k} :
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k) :=
  by
  dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]
  simp

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