isoStrongEpiMono_inv_comp_mono — Mathlib

English

For e,m,comm as above, the inv component of image.isoStrongEpiMono composed with m equals image.ι f.

Русский

Для e,m,comm как выше, обратный компонент image.isoStrongEpiMono после композиции с m равен image.ι f.

LaTeX

$$$(\mathrm{image.isoStrongEpiMono}(e,m,comm)).inv \circ m = \mathrm{image.ι}(f)$$$

Lean4

@[simp]
theorem isoStrongEpiMono_inv_comp_mono {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e] [Mono m] :
    (image.isoStrongEpiMono e m comm).inv ≫ m = image.ι f :=
  image.lift_fac _

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