imageSubobject_factors_comp_self — Mathlib

English

For any k: W → X, the imageSubobject f Factors (k ≫ f) with witness k ≫ factorThruImage f.

Русский

Для любого k: W → X образ подобъекта imageSubobject f факторизуется через k ≫ f с явным фактором k ≫ factorThruImage f.

LaTeX

$$$\mathrm{Factors}\; (\mathrm{imageSubobject} f)\; (k \circ f)$ with witness $k \circ \mathrm{factorThruImage} f$$$

Lean4

theorem imageSubobject_factors_comp_self {W : C} (k : W ⟶ X) : (imageSubobject f).Factors (k ≫ f) :=
  ⟨k ≫ factorThruImage f, by simp⟩

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