explicitCokernelDesc_comp_eq_desc

English

explicitCokernelDesc cond ≫ h = explicitCokernelDesc (f ≫ g ≫ h = 0).

Русский

explicitCokernelDesc cond ≫ h = explicitCokernelDesc (f ≫ g ≫ h = 0).

LaTeX

$$$explicitCokernelDesc(cond) \\\\circ h = explicitCokernelDesc( f \\\\circ g \\\\circ h = 0).$$$

Lean4

theorem explicitCokernelDesc_comp_eq_desc {X Y Z W : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W}
    {cond : f ≫ g = 0} :
    explicitCokernelDesc cond ≫ h =
      explicitCokernelDesc (show f ≫ g ≫ h = 0 by rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]) :=
  by
  refine explicitCokernelDesc_unique _ _ ?_
  rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]

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