skeletal

Mathlib.CategoryTheory.Skeletal

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

English

Skeletal between thin skeleton equivalence and original category is established.

Русский

Установлена скелетность между тонким скелетом и исходной категорией.

LaTeX

$$skeletal : Skeletal (ThinSkeleton C)$$

Lean4

theorem skeletal : Skeletal (ThinSkeleton C) := fun X Y =>
  Quotient.inductionOn₂ X Y fun _ _ h => h.elim fun i => i.1.le.antisymm i.2.le

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

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

Разделы

Аффилиация

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