limitUncurryIsoLimitCompLim_inv_π

English

It is shown that if a cone is constructed via uncurry and the associated data satisfy compatibility, then that cone is universal.

Русский

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

LaTeX

$$$\text{IsLimit}(\text{coneOfConeUncurry } Q c) \Rightarrow \text{IsLimit}(c).$$$

Lean4

@[simp, reassoc]
theorem limitUncurryIsoLimitCompLim_inv_π {j} {k} :
    (limitUncurryIsoLimitCompLim F).inv ≫ limit.π _ (j, k) = (limit.π _ j ≫ limit.π _ k) :=
  by
  rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]
  simp

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