small_subobject

Mathlib.CategoryTheory.Subobject.WellPowered

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

English

The Subobject(X) is a small type when C is LocallySmall and WellPowered.

Русский

Subobject(X) является малым типом при условии LocallySmall и WellPowered.

LaTeX

$$$\mathrm{Small}(\mathrm{Subobject}(X))$$$

Lean4

instance small_subobject [LocallySmall.{w} C] [WellPowered C] (X : C) : Small.{w} (Subobject X) :=
  WellPowered.subobject_small X

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

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

Разделы

Аффилиация

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