isImage — Mathlib

English

The mono-factorisation f has the universal property of the image, i.e., (image, image.ι) together with factorThruImage constitutes an image of f.

Русский

Монофакторизация f обладает универсальным свойством образа; изображение вместе с image.ι и factorThruImage образует образ f.

LaTeX

$$$\\text{IsImage}(\\mathrm{monoFactorisation}(f))$$$

Lean4

/-- The factorisation of any morphism in `ModuleCat R` through a mono has the universal property of
the image. -/
noncomputable def isImage : IsImage (monoFactorisation f)
    where
  lift := image.lift
  lift_fac := image.lift_fac

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