inj_desc — Mathlib

English

For a Cofan IsColimit c, two morphisms f,g: c.pt ⟶ A are equal if and only if for every i, c.inj i ≫ f = c.inj i ≫ g.

Русский

Для кофана IsColimit c две стрелки f,g: c(pt) ⟶ A равны тогда и только тогда, когда для каждого i выполняется c.inj i ≫ f = c.inj i ≫ g.

LaTeX

$$$\\forall i,\\; c.inj i \\; ≫ f = c.inj i \\; ≫ g \\Rightarrow f = g$$$

Lean4

@[reassoc (attr := simp)]
theorem inj_desc {X : β → C} {c : Cofan X} (d : Cofan X) (hc : IsColimit c) (i : β) : c.inj i ≫ hc.desc d = d.inj i :=
  hc.fac _ _

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