isoLimit_hom_π — Mathlib

English

The homomorphism part of the isoLimit is compatible with projections: (Pi.isoLimit X).hom ≫ limit.π (Discrete.mk j) = Pi.π j.

Русский

Часть гомоморфизма у isoLimit совместима с проекциями: (Pi.isoLimit X).hom ≫ limit.π (Discrete.mk j) = Pi.π j.

LaTeX

$$(Pi.isoLimit X).hom ≫ limit.π _ (Discrete.mk j) = Pi.π _ j$$

Lean4

@[reassoc (attr := simp)]
theorem isoLimit_hom_π (j : α) : (Pi.isoLimit X).hom ≫ limit.π _ (Discrete.mk j) = Pi.π _ j :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

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