factorThru_arrow — Mathlib

English

If h is a factorization of f through P, then factorThrough f h composed with P.arrow yields f.

Русский

Если существует факторизация через P, то P.factorThru f h ∘ P.arrow = f.

LaTeX

$$$(P.factorThru f h) \\circ P.arrow = f$$$

Lean4

@[reassoc (attr := simp)]
theorem factorThru_arrow {X Y : C} (P : Subobject Y) (f : X ⟶ Y) (h : Factors P f) : P.factorThru f h ≫ P.arrow = f :=
  Classical.choose_spec ((factors_iff _ _).mp h)

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