isEquivalence_of_iso

Mathlib.CategoryTheory.Equivalence

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

← MathLib Explorer

English

If F ≅ G and F is an equivalence, then G is an equivalence.

Русский

Если F ≅ G и F — эквивалентность, тогда G — эквивалентность.

LaTeX

$$(F ≅ G) implies (IsEquivalence F) implies (IsEquivalence G)$$

Lean4

theorem isEquivalence_of_iso {F G : C ⥤ D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence :=
  ((asEquivalence F).changeFunctor e).isEquivalence_functor

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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