isEquivalence_trans

Mathlib.CategoryTheory.Equivalence

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

English

If F: C ⥤ D and G: D ⥤ E are equivalences, then their composition F ⋙ G is an equivalence.

Русский

Если F: C ⥤ D и G: D ⥤ E — эквивалентности, то их композиция F ⋙ G — эквивалентность.

LaTeX

$$$(F \circ G).IsEquivalence$$$

Lean4

instance isEquivalence_trans (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence G] : IsEquivalence (F ⋙ G) where

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

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

Разделы

Аффилиация

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