hasStrongEpiImages_of_hasStrongEpiMonoFactorisations

English

If HasStrongEpiMonoFactorisations C, then HasStrongEpiImages C.

Русский

Если в категории C существуют сильные эпиморфно-монографические факторизации, то существуют сильные эпиморфные образы.

LaTeX

$$$\mathrm{HasStrongEpiImages}(C)$$$

Lean4

/-- If we constructed our images from strong epi-mono factorisations, then these images are
strong epi images. -/
instance (priority := 100) hasStrongEpiImages_of_hasStrongEpiMonoFactorisations [HasStrongEpiMonoFactorisations C] :
    HasStrongEpiImages C where
  strong_factorThruImage
    f :=
    strongEpi_factorThruImage_of_strongEpiMonoFactorisation <|
      Classical.choice <| HasStrongEpiMonoFactorisations.has_fac f

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