strongEpiCategory_of_regularEpiCategory

English

If C is a regular epi category, then it is a StrongEpiCategory.

Русский

Если C является категорией регулярных эпиморфизмов, то она является StrongEpiCategory.

LaTeX

$$[IsRegularEpiCategory C] ⇒ [StrongEpiCategory C]$$

Lean4

instance (priority := 100) strongEpiCategory_of_regularEpiCategory [IsRegularEpiCategory C] : StrongEpiCategory C where
  strongEpi_of_epi f
    _ := by
    haveI := regularEpiOfEpi f
    infer_instance

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