hasColimitsOfShape_widePushoutShape

English

If J is finite and C has finite wide pushouts, then HasColimitsOfShape(WidePushoutShape J) C.

Русский

Если J конечен и в C существуют конечные широкие пушупы, тогда HasColimitsOfShape(WidePushoutShape J) C.

LaTeX

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

Lean4

instance hasColimitsOfShape_widePushoutShape (J : Type) [Finite J] [HasFiniteWidePushouts C] :
    HasColimitsOfShape (WidePushoutShape J) C :=
  by
  haveI := @HasFiniteWidePushouts.out C _ _ J
  infer_instance

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