compIso_hom_comp_image_ι — Mathlib

English

The composition (image.compIso f g).hom ≫ image.ι (f ≫ g) equals image.ι f ≫ g.

Русский

Составление (image.compIso f g).hom ≫ image.ι (f ≫ g) равно image.ι f ≫ g.

LaTeX

$$$ (\\mathrm{image}.\\mathrm{compIso}(f,g)).\\mathrm{hom} \\circ \\mathrm{image}.\\iota(f \\circ g) = \\mathrm{image}.\\iota(f) \\circ g $$$

Lean4

@[reassoc (attr := simp)]
theorem compIso_hom_comp_image_ι [HasImage f] [IsIso g] : (image.compIso f g).hom ≫ image.ι (f ≫ g) = image.ι f ≫ g :=
  by
  ext
  simp [image.compIso]

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