hasLimitsOfShape_widePullbackShape

English

If J is finite and C has finite wide pullbacks, then HasLimitsOfShape(WidePullbackShape J) C.

Русский

Если J конечен и в C существуют конечные широкие вытяжки, тогда HasLimitsOfShape(WidePullbackShape J) C.

LaTeX

$$$\forall J\,[\text{Finite }J] \Rightarrow \operatorname{HasLimitsOfShape}(\mathrm{WidePullbackShape}(J), C)$$$

Lean4

instance hasLimitsOfShape_widePullbackShape (J : Type) [Finite J] [HasFiniteWidePullbacks C] :
    HasLimitsOfShape (WidePullbackShape J) C :=
  by
  haveI := @HasFiniteWidePullbacks.out C _ _ J
  infer_instance

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