map_ι — Mathlib

English

The interaction of image map with the inclusion maps is compatible: image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right.

Русский

Взаимодействие отображения образа с инклюзивными отображениями совместимо: image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right.

LaTeX

$$$\mathrm{image.map}(sq) \circ \mathrm{image.\iota}(g.hom) = \mathrm{image.\iota}(f.hom) \circ sq.right$$$

Lean4

theorem map_ι : image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right := by simp

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