isoInverseOfIsoFunctor_isoFunctorOfIsoInverse

English

The inverse of the inverse of a functor iso is the original iso: isoInverseOfIsoFunctor (isoFunctorOfIsoInverse i) = i.

Русский

Обратная к обратной функтору изоморфности равна самой исходной изоморфности.

LaTeX

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

Lean4

@[simp]
theorem isoInverseOfIsoFunctor_isoFunctorOfIsoInverse {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) :
    isoInverseOfIsoFunctor (isoFunctorOfIsoInverse i) = i :=
  isoFunctorOfIsoInverse_isoInverseOfIsoFunctor (G := G.symm) (G' := G'.symm) i

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