strongEpi_factorThruImage_of_strongEpiMonoFactorisation

English

If F is a StrongEpiMonoFactorisation f, then factorThruImage f is strong epi.

Русский

Если F является сильной epi-монo факторизацией для f, то factorThruImage f является сильной epi.

LaTeX

$$$\operatorname{StrongEpi}(\operatorname{factorThruImage}(f))$$$

Lean4

theorem strongEpi_factorThruImage_of_strongEpiMonoFactorisation {X Y : C} {f : X ⟶ Y} [HasImage f]
    (F : StrongEpiMonoFactorisation f) : StrongEpi (factorThruImage f) :=
  strongEpi_of_strongEpiMonoFactorisation F <| Image.isImage f

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