comp_preservesCofilteredLimits — Mathlib

English

If F preserves cofiltered limits and G preserves cofiltered limits, then F ⋙ G preserves cofiltered limits.

Русский

Если F сохраняет кофильтрованные пределы, и G сохраняет их, тогда F ⋙ G сохраняет их.

LaTeX

$$$PreservesCofilteredLimitsOfSize.{w, w'} (F ⋙ G)$$$

Lean4

instance comp_preservesCofilteredLimits (F : C ⥤ D) (G : D ⥤ E) [PreservesCofilteredLimitsOfSize.{w, w'} F]
    [PreservesCofilteredLimitsOfSize.{w, w'} G] : PreservesCofilteredLimitsOfSize.{w, w'} (F ⋙ G) where
  preserves_cofiltered_limits _ := inferInstance

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