limitIsoLimitCurryCompLim_inv_π — Mathlib

English

The inverse of the limit iso satisfies π_(j,k) = π_j ∘ π_k after application.

Русский

Обратное итого предел-изоморфизма удовлетворяет выражение π_(j,k) = π_j ∘ π_k после применения.

LaTeX

$$$(\text{limitIsoLimitCurryCompLim } G).inv ∘ \text{limit.π}_{(j,k)} = \text{limit.π}_j ∘ \text{limit.π}_k$$$

Lean4

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

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