factorThruImage_preComp — Mathlib

English

For f,g with HasImage g and HasImage (f ≫ g), factorThruImage (f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g.

Русский

Для f,g с HasImage g и HasImage (f ≫ g): factorThruImage(f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g.

LaTeX

$$$ \\mathrm{factorThruImage}(f\\gg) \\; \\circ \\; \\mathrm{image.preComp}(f,g) = f \\circ \\mathrm{factorThruImage}(g) $$$

Lean4

@[reassoc (attr := simp)]
theorem factorThruImage_preComp [HasImage g] [HasImage (f ≫ g)] :
    factorThruImage (f ≫ g) ≫ image.preComp f g = f ≫ factorThruImage g := by simp [image.preComp]

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