fac — Mathlib

English

If c is a colimit cocone for a cofan F : β → C, and f_i : F i ⟶ A, then c.inj i ≫ Cofan.IsColimit.desc hc f = f_i.

Русский

Пусть c является колимитным кононом для кофана F: β → C; тогда для любой семейки f_i: F i ⟶ A верно c.inj i ≫ desc hc f = f_i.

LaTeX

$$$\\forall i,\\; c.inj i \\; ≫ \\; \\mathrm{Cofan.IsColimit.desc}\\ hc f = f_i$$$

Lean4

@[reassoc (attr := simp)]
theorem fac {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f : ∀ i, F i ⟶ A) (i : β) :
    c.inj i ≫ Cofan.IsColimit.desc hc f = f i :=
  hc.fac (Cofan.mk A f) ⟨i⟩

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