sup_factors_of_factors_left — Mathlib

English

Let A,B be objects of C and X,Y be subobjects of B. If X factors through a morphism f: A → B, then the join X ⊔ Y also factors through f.

Русский

Пусть A,B — объекты, а X,Y — подпредметы B. Если X факторизуется через морфизм f: A → B, тогда объединение X ⊔ Y также факторизуется через f.

LaTeX

$$$(X \sqcup Y).\mathrm{Factors}(f)$, если $X.factors(f)$, следовательно $(X \sqcup Y).Factors f$.$$

Lean4

theorem sup_factors_of_factors_left {A B : C} {X Y : Subobject B} {f : A ⟶ B} (P : X.Factors f) : (X ⊔ Y).Factors f :=
  factors_of_le f le_sup_left P

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