has_cofiltered_limits_of_has_filtered_colimits_op

English

If C^op has filtered colimits, then C has cofiltered limits.

Русский

Если в Opposite C существуют отфильтрованные колимиты, то в C существуют ко-филтированные пределы.

LaTeX

$$$$\\mathrm{HasCofilteredLimitsOfSize}(C) \\;\\text{from}\\; \\mathrm{HasFilteredColimitsOfSize}(C^{op}).$$$$

Lean4

theorem has_cofiltered_limits_of_has_filtered_colimits_op [HasFilteredColimitsOfSize.{v₂, u₂} Cᵒᵖ] :
    HasCofilteredLimitsOfSize.{v₂, u₂} C :=
  { HasLimitsOfShape := fun _ _ _ => hasLimitsOfShape_of_hasColimitsOfShape_op }

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