fromThinSkeleton_isEquivalence

Mathlib.CategoryTheory.Skeletal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence

English

The equivalence between ThinSkeleton and C is itself an equivalence of functors.

Русский

Эквивалентость между ThinSkeleton и C является эквивалентностью функторов.

LaTeX

$$equivalence .IsEquivalence := ...$$

Lean4

noncomputable instance fromThinSkeleton_isEquivalence : (fromThinSkeleton C).IsEquivalence :=
  (equivalence C).isEquivalence_functor

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

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

Разделы

Аффилиация

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