skeleton_isSkeleton

Mathlib.CategoryTheory.Skeletal

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

← MathLib Explorer

English

The skeleton is a skeleton of C via fromSkeleton.

Русский

Скелетон является скелетом C через fromSkeleton.

LaTeX

$$$\mathrm{IsSkeletonOf}\; C\; (\mathrm{Skeleton}(C))\; (\mathrm{fromSkeleton}(C))$$$

Lean4

/-- The `skeleton` of `C` given by choice is a skeleton of `C`. -/
theorem skeleton_isSkeleton : IsSkeletonOf C (Skeleton C) (fromSkeleton C)
    where
  skel := skeleton_skeletal C
  eqv := fromSkeleton.isEquivalence C

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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