comp_coconePointUniqueUpToIso_hom

English

For colimits s,t and j in J, the leg s.ι.app j composed with the isomorphism coconePointUniqueUpToIso P Q equals w.hom.app j composed with t.ι.app j.

Русский

Для колимитов s,t и любого j ∈ J, композиция s.ι.app j с изоморфизмом coconePointUniqueUpToIso(P,Q) равна композиции w.hom.app j с t.ι.app j.

LaTeX

$$$ s.ι.app j \;≫\; (P.coconePointUniqueUpToIso Q).hom = w.hom.app j \;≫\; t.ι.app j $$$

Lean4

@[reassoc (attr := simp)]
theorem comp_coconePointUniqueUpToIso_hom {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) :
    s.ι.app j ≫ (coconePointUniqueUpToIso P Q).hom = t.ι.app j :=
  (uniqueUpToIso P Q).hom.w _

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