essentiallySmall_fullSubcategory_mem

English

If s ⊆ C and s.Elem is small and C is locally small, then the full subcategory on elements of s is essentially small.

Русский

Если s ⊆ C и s.Elem мал, и C локально мал, то полная подкатегория объектов, принадлежащих s, является существенно малой.

LaTeX

$$$\text{EssentiallySmall}(\text{ObjectProperty.FullSubcategory}(\cdot \in s))$$$

Lean4

instance essentiallySmall_fullSubcategory_mem (s : Set C) [Small.{w} s] [LocallySmall.{w} C] :
    EssentiallySmall.{w} (ObjectProperty.FullSubcategory (· ∈ s)) :=
  suffices Small.{w} (ObjectProperty.FullSubcategory (· ∈ s)) from essentiallySmall_of_small_of_locallySmall _
  small_of_injective (f := fun x => (⟨x.1, x.2⟩ : s)) (by cat_disch)

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