compIso_inv_comp_image_ι — Mathlib

English

The inverse part of the image compIso satisfies (image.compIso f g).inv ≫ image.ι f = image.ι (f ≫ g) ≫ inv g.

Русский

Обратная часть image.compIso f g удовлетворяет (image.compIso f g).inv ≫ image.ι f = image.ι (f ≫ g) ≫ inv g.

LaTeX

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

Lean4

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

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