factors_right_of_factors_add — Mathlib

English

In a preadditive setting, if f and g factor through P, then their sum factors through P.

Русский

В предадитивной обстановке сумма факторизуется через P, если f и g факторизуются через P.

LaTeX

$$$P.\text{Factors} (f+g)$$$

Lean4

theorem factors_right_of_factors_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g))
    (wf : P.Factors f) : P.Factors g :=
  (factors_iff _ _).mpr ⟨P.factorThru (f + g) w - P.factorThru f wf, by simp⟩

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