toSkeleton_fromSkeleton_obj

Mathlib.CategoryTheory.Skeletal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.toSkeleton_fromSkeleton_obj

English

For any X in Skeleton C, the toSkeleton of the image of X under fromSkeleton C equals X.

Русский

Для любого X в Skeleton C toSkeleton((fromSkeleton C).obj X) = X.

LaTeX

$$$toSkeleton((fromSkeleton C).obj X) = X$$$

Lean4

theorem toSkeleton_fromSkeleton_obj (X : Skeleton C) : toSkeleton ((fromSkeleton C).obj X) = X :=
  Quotient.out_eq _

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

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

Разделы

Аффилиация

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