instEssentiallySmallFullSubcategoryCofilteredClosure

English

The full subcategory induced by cofilteredClosure f is essentially small.

Русский

Полная подпредкатегория кофильтрованного замыкания является по существу малой.

LaTeX

$$$\\operatorname{EssentiallySmall}((\\mathrm{cofilteredClosure} f).\\mathrm{FullSubcategory})$$$

Lean4

instance : EssentiallySmall.{max v w} (cofilteredClosure f).FullSubcategory :=
  have : LocallySmall.{max v w} (cofilteredClosure f).FullSubcategory := locallySmall_max.{w, v, u}
  have := small_fullSubcategory_cofilteredClosure f
  essentiallySmall_of_small_of_locallySmall _

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