hasExactLimitsOfShape_discrete_finite

English

Exact limits for discrete finite shapes hold in the opposite category as well.

Русский

Точность пределов для дискретных конечных форм сохраняется и в противоположной категории.

LaTeX

$$$\\operatorname{HasExactLimitsOfShape}(\\Discrete J) C \\Rightarrow \\operatorname{HasExactLimitsOfShape}(\\Discrete J)^{op} C$$$

Lean4

noncomputable instance hasExactLimitsOfShape_discrete_finite {J : Type*} [Finite J] :
    HasExactLimitsOfShape (Discrete J) C where
  preservesFiniteColimits := preservesFiniteColimits_of_natIso HasBiproductsOfShape.colimIsoLim

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