colimitOpIsoOpLimit — Mathlib

English

If Opposite C has filtered colimits, then C has cofiltered limits.

Русский

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

LaTeX

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

Lean4

/-- The colimit of `F.op` is the opposite of `limit F`. -/
def colimitOpIsoOpLimit (F : J ⥤ C) [HasLimit F] : colimit F.op ≅ op (limit F) :=
  colimit.isoColimitCocone ⟨_, (limit.isLimit _).op⟩

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