reflectsCofilteredLimits — Mathlib

English

If a functor F reflects limits of a given size, then it reflects cofiltered limits of that size.

Русский

Если функтор F отражает пределы заданного размера, то он отражает когильтрованные пределы этого размера.

LaTeX

$$$\text{ReflectsCofilteredLimitsOfSize}(F; w, w')$$$

Lean4

instance (priority := 100) reflectsCofilteredLimits (F : C ⥤ D) [ReflectsLimitsOfSize.{w, w'} F] :
    ReflectsCofilteredLimitsOfSize.{w, w'} F where reflects_cofiltered_limits _ := inferInstance

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