isEquivalence_inv

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.isEquivalence_inv

English

If F: C ⥤ D is an equivalence, then its inverse F^{-1} is an equivalence.

Русский

Пусть F: C ⥤ D является эквивалентностью; тогда F^{-1} также эквивалентна.

LaTeX

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

Lean4

instance isEquivalence_inv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv :=
  F.asEquivalence.symm.isEquivalence_functor

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru