instEssentiallySmallFullSubcategoryFilteredClosure

English

The full subcategory from filteredClosure is essentially small when IsFilteredOrEmpty holds.

Русский

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

LaTeX

$$$[IsFilteredOrEmpty C] \Rightarrow \text{EssentiallySmall}(\text{filteredClosure } f).\text{FullSubcategory}$$$

Lean4

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

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