factor_map — Mathlib

English

The factorization through the image interacts with the image map: factorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom.

Русский

Факторизация через образ взаимодействует с отображением образа: factorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom.

LaTeX

$$$\operatorname{factorThruImage}(f.hom) \circ \mathrm{image.map}(sq) = sq.left \circ \operatorname{factorThruImage}(g.hom)$$$

Lean4

theorem factor_map : factorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom := by simp

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