preservesCofilteredLimits — Mathlib

English

If F preserves limits of size w', w, then F preserves cofiltered limits of size w, w'.

Русский

Если F сохраняет пределы размерa w', w, то F сохраняет кофильтрованные пределы размера w, w'.

LaTeX

$$$PreservesCofilteredLimitsOfSize.{w, w'} F$$$

Lean4

instance (priority := 100) preservesCofilteredLimits (F : C ⥤ D) [PreservesLimitsOfSize.{w, w'} F] :
    PreservesCofilteredLimitsOfSize.{w, w'} F where preserves_cofiltered_limits _ := inferInstance

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