limitIsoOfIsRightKanExtension_inv_π

English

For each i in C, (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i.

Русский

Для каждого i в C выполняется: (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i.

LaTeX

$$$(F'.limitIsoOfIsRightKanExtension\\ α).inv \\;\\circ\\; \\text{limit.π}_F'(L.obj i) \\;\\circ\\; α.app i = \\text{limit.π}_F i$$$

Lean4

@[reassoc (attr := simp)]
theorem limitIsoOfIsRightKanExtension_inv_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i := by
  simp [limitIsoOfIsRightKanExtension]

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