instLocallySmallObjAsType — Mathlib

English

If α is a countable category, then ObjAsType(α) is locally small; in particular, for any two objects X,Y in ObjAsType(α), the hom-set Hom(X,Y) is a set.

Русский

Если α — счетная категория, то ObjAsType(α) локально мала; в частности, для любых объектов X,Y в ObjAsType(α) множество гомоморизмов Hom(X,Y) является множеством.

LaTeX

$$$\operatorname{LocallySmall}(\mathrm{ObjAsType}(\alpha))$$$

Lean4

instance : LocallySmall.{0} (ObjAsType α) where hom_small _ _ := inferInstance

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