instIsEquivalenceInverse

Mathlib.CategoryTheory.EssentiallySmall

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShrinkHoms.instIsEquivalenceInverse

English

The inverse ShrinkHoms functor is an equivalence.

Русский

Обратный функтор ShrinkHoms является эквивалентностью.

LaTeX

$$$(\mathrm{ShrinkHoms}.inverse\, C).IsEquivalence$$$

Lean4

instance : (inverse C).IsEquivalence :=
  (equivalence C).isEquivalence_inverse

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru