factorThruImageSubobject_comp_self_assoc

English

A associativity variant for factorThruImageSubobject: combining k and k' yields k ≫ k' ≫ factorThruImageSubobject f.

Русский

Вариант ассоциативности факторизации: объединение k и k' даёт k ≫ k' ≫ factorThruImageSubobject f.

LaTeX

$$$((\mathrm{imageSubobject} f).factorThru (k ≫ k' ≫ f)) = (k ≫ k') ≫ \mathrm{factorThruImageSubobject} f$$$

Lean4

@[simp]
theorem factorThruImageSubobject_comp_self_assoc {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X) (h) :
    (imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f :=
  by
  ext
  simp

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