limitFlipCompLimIsoLimitCompLim_inv_π_π

English

Inverse of the limit iso respects projection on (j,k).

Русский

Обратное от предел-изоморфизма сохраняет проекцию на (j,k).

LaTeX

$$$(limitUncurryIsoLimitCompLim F)^{-1} \circ limit.π_{(j,k)} = limit.π_j \circ limit.π_k$$$

Lean4

@[simp, reassoc]
theorem limitFlipCompLimIsoLimitCompLim_inv_π_π (k) (j) :
    (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π _ k ≫ limit.π _ j = (limit.π _ j ≫ limit.π _ k) := by
  simp [limitFlipCompLimIsoLimitCompLim]

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