rightUnitor_isEquivalence — Mathlib

English

The right unitor functor is an equivalence of categories with its inverse given by the right inverse unitor.

Русский

Правый унитор-функтор образует эквивалентность категорий, а его обратной связью служит правый обратный унитор.

LaTeX

$$$(\\mathrm{rightUnitor} \\mathcal{C}).IsEquivalence$$$

Lean4

instance rightUnitor_isEquivalence : (rightUnitor C).IsEquivalence :=
  (rightUnitorEquivalence C).isEquivalence_functor

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