instFaithfulSkeletonMapSkeleton

Mathlib.CategoryTheory.Skeletal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instFaithfulSkeletonMapSkeleton

English

If F is faithful, then F.mapSkeleton.Faithful holds.

Русский

Если F верен, то F.mapSkeleton.Faithful выполняется.

LaTeX

$$$F.mapSkeleton.Faithful$$$

Lean4

instance [F.Faithful] : F.mapSkeleton.Faithful := by unfold mapSkeleton; infer_instance

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

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

Разделы

Аффилиация

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