isoLimitCone_inv_π — Mathlib

English

For t: LimitCone F, the inv component of limit.isoLimitCone t composed with π_j equals t.cone.π.app j.

Русский

Для t: LimitCone F, inv часть limit.isoLimitCone t, умноженная на π_j, равна t.cone.π.app j.

LaTeX

$$$(\\mathrm{limit}.isoLimitCone t).inv \\;\\circ\\; \\mathrm{limit}.π F j = t.cone.π.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem isoLimitCone_inv_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).inv ≫ limit.π F j = t.cone.π.app j :=
  by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  simp

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