locallySmall_self

Mathlib.CategoryTheory.EssentiallySmall

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

English

LocallySmall holds for any category C with a category structure.

Русский

LocallySmall держится для любой категории C с структурой категории.

LaTeX

$$$\operatorname{LocallySmall}(C)$$$

Lean4

instance (priority := 100) locallySmall_self (C : Type u) [Category.{v} C] : LocallySmall.{v} C where

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

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

Разделы

Аффилиация

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