small_skeleton_of_essentiallySmall

Mathlib.CategoryTheory.EssentiallySmall

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

English

If a category C is essentially small, then its skeleton is small.

Русский

Если C является существенно малой, тогда его скелетон мал.

LaTeX

$$$\text{EssentiallySmall}(C) \Rightarrow \text{Small}(\text{Skeleton}(C))$$$

Lean4

instance small_skeleton_of_essentiallySmall [h : EssentiallySmall.{w} C] : Small.{w} (Skeleton C) :=
  essentiallySmall_iff C |>.1 h |>.1

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

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

Разделы

Аффилиация

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