instIsEquivalenceObjWhiskeringRight

English

If F: C ⥤ D is an equivalence, then whiskering on the right by E yields an equivalence.

Русский

Если F: C ⥤ D — эквивалентность, то правое взвешивание F по отношению к E даёт эквивалентность.

LaTeX

$$$\bigl((\mathrm{whiskeringRight}\ E\ C\ D).\mathrm{obj} F\bigr).IsEquivalence$$$

Lean4

instance (F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringRight E C D).obj F) :=
  (inferInstance : IsEquivalence (Equivalence.congrRight F.asEquivalence).functor)

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