preservesLimitsOfSize_op — Mathlib

English

If F: C ⥤ D preserves colimits of all sizes, then F.op: C^{op} ⥤ D^{op} preserves limits of all sizes.

Русский

Если F: C ⥤ D сохраняет колимиты во всех размерах, тогда F.op: C^{op} ⥤ D^{op} сохраняет предельные копии во всех размерах.

LaTeX

$$$(F: C \to D) [PreservesColimitsOfSize(F)] \Rightarrow (F^{op}: C^{op} \to D^{op}) [PreservesLimitsOfSize(F.op)].$$$

Lean4

/-- If `F : C ⥤ D` preserves colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits. -/
theorem preservesLimitsOfSize_op (F : C ⥤ D) [PreservesColimitsOfSize.{w, w'} F] : PreservesLimitsOfSize.{w, w'} F.op
    where preservesLimitsOfShape {_} _ := preservesLimitsOfShape_op _ _

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