locallySmall_max

Mathlib.CategoryTheory.EssentiallySmall

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

English

LocallySmall holds for C in the maximal universe setting.

Русский

LocallySmall держится для C в максимальном уровне вселенной.

LaTeX

$$$\operatorname{LocallySmall}(C)$ in the maximal universe context$$

Lean4

theorem locallySmall_max {C : Type u} [Category.{v} C] : LocallySmall.{max v w} C where hom_small _ _ := small_max.{w} _

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

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

Разделы

Аффилиация

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