instIsEquivalenceObjWhiskeringLeft

English

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

Русский

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

LaTeX

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

Lean4

instance (F : C ⥤ D) [IsEquivalence F] : IsEquivalence ((whiskeringLeft C D E).obj F) :=
  (inferInstance : IsEquivalence (Equivalence.congrLeft F.asEquivalence).inverse)

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