instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor

English

There is a limit for the composed functor ((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op) under HasCoproduct Z.

Русский

Существует предел для композиции ((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op) при HasCoproduct Z.

LaTeX

$$$\\text{HasLimit}((\\mathrm{Discrete.opposite } α).inverse \\circ (\\mathrm{Discrete.functor } Z)^{\\mathrm{op}})$$$

Lean4

instance : HasLimit ((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op) :=
  hasLimit_equivalence_comp (Discrete.opposite α).symm

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