instFullSkeletonFromSkeleton

Mathlib.CategoryTheory.Skeletal

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

English

The skeleton of C, obtained by choice, has a full embedding into C.

Русский

Скелетон C, полученный по выбору, инъективно полно отображает C.

LaTeX

$$$(fromSkeleton\, C).Full$$$

Lean4

noncomputable instance : (fromSkeleton C).Full := by apply InducedCategory.full

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

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

Разделы

Аффилиация

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