ι_desc — Mathlib

English

Let f: β → C with HasCoproduct f and P. For p: ∀ b, f(b) ⟶ P, the j-th injection composed with Sigma.desc p equals p(b).

Русский

Пусть f: β → C имеет копроизведение и P. Для p: ∀ b, f(b) ⟶ P, композиция ι_b с Sigma.desc p равна p(b).

LaTeX

$$$\forall b:\, β,\Sigma.ι f b \;\;≫\; \Sigma.desc p = p b$$$

Lean4

@[reassoc]
theorem ι_desc {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) (b : β) :
    Sigma.ι f b ≫ Sigma.desc p = p b := by simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

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