hasFiniteWidePushouts_of_has_finite_limits

English

If C has finite colimits, then C has finite wide pushouts.

Русский

Если в C существуют конечные колимиты, то существуют конечные широкие пушупы.

LaTeX

$$$\operatorname{HasFiniteColimits}(C) \Rightarrow \operatorname{HasFiniteWidePushouts}(C)$$$

Lean4

/-- Finite wide pushouts are finite colimits, so if `C` has all finite colimits,
it also has finite wide pushouts
-/
instance (priority := 900) hasFiniteWidePushouts_of_has_finite_limits [HasFiniteColimits C] : HasFiniteWidePushouts C :=
  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteColimits.out _⟩

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