isEquivalence_mapArrow — Mathlib

English

If F: C ⥤ D is an equivalence, then the induced arrow functor F.mapArrow is also an equivalence.

Русский

Если F: C ⥤ D является эквивалентностью, то индуцированная стрелочная функция F.mapArrow также эквивалентна.

LaTeX

$$$\text{IsEquivalence}(F.mapArrow)$$$

Lean4

instance isEquivalence_mapArrow (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.mapArrow :=
  (mapArrowEquivalence (asEquivalence F)).isEquivalence_functor

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