opFunctorCompOpFunctorIso_inv_app_app

English

Similarly for the inverse component of the opFunctorCompOpFunctorIso: the inv app equals the composition of opObjIso.inv with itself.

Русский

Аналогично для обратной компоненты opFunctorCompOpFunctorIso: inv.app равен композиции opObjIso.inv с самим собой.

LaTeX

$$(opFunctorCompOpFunctorIso.inv.app X).app n = opObjIso.inv \circ opObjIso.inv$$

Lean4

@[simp]
theorem opFunctorCompOpFunctorIso_inv_app_app (X : SimplicialObject C) (n : SimplexCategoryᵒᵖ) :
    (opFunctorCompOpFunctorIso.inv.app X).app n = opObjIso.inv ≫ opObjIso.inv := by
  simp [opFunctorCompOpFunctorIso, opObjIso, opFunctor]

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