isLimitEquivIsColimitOp — Mathlib

English

For any cone t, t is a limit cone if and only if its opposite cocone t.op is a colimit cocone.

Русский

Для любого конуса t он является пределом тогда и только тогда, когда противоположный конус t.op является ко-лимитом.

LaTeX

$$$ \text{IsLimit}(t) \cong \text{IsColimit}(t^{op}) \quad (t : \text{Cone } F). $$$

Lean4

/-- `t : Cone F` is a limit cone if and only if `t.op : Cocone F.op` is a colimit cocone.
-/
def isLimitEquivIsColimitOp {t : Cone F} : IsLimit t ≃ IsColimit t.op :=
  equivOfSubsingletonOfSubsingleton IsLimit.op isLimitOfOp

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