conePointsIsoOfNatIso_inv_comp — Mathlib

English

Similarly, (conePointsIsoOfNatIso P Q w).inv ≪comp≫ s.π.app j = t.π.app j ≪comp≫ w.inv.app j for all j.

Русский

Аналогично, (conePointsIsoOfNatIso P Q w).inv композицией дает: (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j.

LaTeX

$$$ (conePointsIsoOfNatIso\, P\, Q\, w).inv \\circ s.π_{j} = t.π_{j} \\circ w.inv_{j} $$$

Lean4

@[reassoc]
theorem conePointsIsoOfNatIso_inv_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
    (w : F ≅ G) (j : J) : (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j := by simp

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