coproductIsCoproduct' — Mathlib

English

Auxiliary equality used in establishing that the Sigma.cocone is a colimit cocone.

Русский

Вспомогательное равенство, используемое при доказательстве, что Sigma.cocone является колимитным кононом.

LaTeX

$$$\\text{auxiliary equalities within the colimit proof}$$$

Lean4

/-- The cocone `Sigma.cocone X` is a colimit cocone. -/
def coproductIsCoproduct' : IsColimit (Sigma.cocone X)
    where
  desc s := Sigma.desc (fun j => s.ι.app ⟨j⟩)
  fac s := by simp
  uniq s m
    hm := by
    dsimp
    ext
    simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
    apply hm

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