isEquivalence_inverse — Mathlib

English

Let F: C ≌ D be an equivalence of categories. Then the inverse functor F^{-1} is itself an equivalence.

Русский

Пусть F: C ⥤ D — эквивалентность категорий. Тогда обратный к F функтор F^{-1} тоже является эквивалентностью.

LaTeX

$$$\operatorname{IsEquivalence}(F^{-1}).$$$

Lean4

instance isEquivalence_inverse (F : C ≌ D) : IsEquivalence F.inverse :=
  F.symm.isEquivalence_functor

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