factorThru_ofLE — Mathlib

English

If P ≤ Q are subobjects of Y and f: Z → Y with w a factorization of f through P, then the factorThrough through Q is given by Q.factorThru f (factors_of_le f h w) and equals P.factorThru f w composed with the inclusion P ≤ Q.

Русский

Пусть P ≤ Q — подпредметы Y, f: Z → Y; если w — факторизация f через P, тогда Q.factorThru f (...)= P.factorThru f w ⋅ ofLE P Q h.

LaTeX

$$$Q.\text{factorThru} f (\text{factors_of_le } f h w) = P.\text{factorThru} f w \;\circ\; \text{ofLE } P Q h$$$

Lean4

theorem factorThru_ofLE {Y Z : C} {P Q : Subobject Y} {f : Z ⟶ Y} (h : P ≤ Q) (w : P.Factors f) :
    Q.factorThru f (factors_of_le f h w) = P.factorThru f w ≫ ofLE P Q h :=
  by
  ext
  simp

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