toThinSkeleton_faithful

Mathlib.CategoryTheory.Skeletal

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

English

The functor from ThinSkeleton to itself is faithful via a suitable equivalence.

Русский

Функтор между тонким скелетом и самим собой является верным через подходящую эквивалентность.

LaTeX

$$toThinSkeleton_faithful : (toThinSkeleton C).Faithful$$

Lean4

instance toThinSkeleton_faithful : (toThinSkeleton C).Faithful where

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

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

Разделы

Аффилиация

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