of_isColimit — Mathlib

English

If c is a colimit cocone for the pushout, then the corresponding IsPushout structure holds for f,g with c.inl, c.inr.

Русский

Если c является аккумуляторным колимитом кокон для объединения (Pushout), то структура IsPushout для f,g с c.inl, c.inr верна.

LaTeX

$$$ IsColimit c \Rightarrow IsPushout f g c.inl c.inr $$$

Lean4

/-- If `c` is a colimiting pushout cocone, then we have an `IsPushout f g c.inl c.inr`. -/
theorem of_isColimit {c : PushoutCocone f g} (h : Limits.IsColimit c) : IsPushout f g c.inl c.inr :=
  { w := c.condition
    isColimit' := ⟨IsColimit.ofIsoColimit h (Limits.PushoutCocone.ext (Iso.refl _) (by simp) (by simp))⟩ }

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