sup_factors_of_factors_right — Mathlib

English

Let A,B be objects and X,Y be subobjects of B. If Y factors through f: A → B, then (X ⊔ Y) factors through f.

Русский

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

LaTeX

$$$(X \sqcup Y).Factors f$ если $Y.Factors f$.$$

Lean4

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

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