skeleton_skeletal

Mathlib.CategoryTheory.Skeletal

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

← MathLib Explorer

English

The skeleton of the skeleton of C is skeletal: Skeletal (Skeleton C).

Русский

Скелетон скелета C есть Skeletal (Skeleton C).

LaTeX

$$$\mathrm{Skeletal}(\mathrm{Skeleton}(C))$$$

Lean4

theorem skeleton_skeletal : Skeletal (Skeleton C) :=
  by
  rintro X Y ⟨h⟩
  have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
  simpa using Quotient.sound this

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

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

Разделы

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

Аффилиация

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