locallySmall_fullSubcategory — Mathlib

English

If C is locally small and P is an object property, then the full subcategory of P is locally small.

Русский

Если C локально малaя, и P — свойство объектов, то полная подкатегория объектов, удовлетворяющих P, локально малая.

LaTeX

$$$\operatorname{LocallySmall}(P.\mathrm{FullSubcategory})$$$

Lean4

instance locallySmall_fullSubcategory [LocallySmall.{w} C] (P : ObjectProperty C) :
    LocallySmall.{w} P.FullSubcategory :=
  locallySmall_of_faithful <| P.ι

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