factorThru_zero — Mathlib

English

If P ⊆ Y and f factors through P via h, then P.factorThru 0 h = 0.

Русский

Если P ⊆ Y и f факторизуется через P с помощью h, то P.factorThru 0 h = 0.

LaTeX

$$$P\!\text{.factorThru}(0,h) = 0$$$

Lean4

@[simp]
theorem factorThru_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y} (h : P.Factors (0 : X ⟶ Y)) :
    P.factorThru 0 h = 0 := by
  simp
    -- `h` is an explicit argument here so we can use
    -- `rw factorThru_ofLE h`, obtaining a subgoal `P.Factors f`.
    -- (While the reverse direction looks plausible as a simp lemma, it seems to be unproductive.)

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