isoFunctorOfIsoInverse_isoInverseOfIsoFunctor

English

Sanity check: isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) equals i.

Русский

Проверка: isoFunctorOfIsoInverse(isoInverseOfIsoFunctor i) равняется i.

LaTeX

$$$\operatorname{isoFunctorOfIsoInverse}(\operatorname{isoInverseOfIsoFunctor}(i)) = i$$$

Lean4

/-- Sanity check: `isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i)` is just `i`. -/
@[simp]
theorem isoFunctorOfIsoInverse_isoInverseOfIsoFunctor {G G' : C ≌ D} (i : G.functor ≅ G'.functor) :
    isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i) = i :=
  by
  ext X
  simp [← NatTrans.naturality]

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