isEquivalenceMapPair — Mathlib

English

If F : C ⥤ C′ and F′ : D ⥤ D′ are equivalences, then the induced functor mapPair F F′ : Join C D ⥤ Join C′ D′ is an equivalence.

Русский

Если F : C ⥤ C′ и F′ : D ⥤ D′ являются эквивалентностями, то индуцированное отображение mapPair F F′: Join C D ⥤ Join C′ D′ является эквивалентностью.

LaTeX

$$$\operatorname{mapPair} F F' \;\text{is an equivalence}$$$

Lean4

instance isEquivalenceMapPair {F : C ⥤ C'} {F' : D ⥤ D'} [F.IsEquivalence] [F'.IsEquivalence] :
    (mapPair F F').IsEquivalence :=
  inferInstanceAs (mapPairEquiv F.asEquivalence F'.asEquivalence).functor.IsEquivalence

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