strongEpi_of_epi — Mathlib

English

In a category with the StrongEpiCategory structure, every epi is a strong epi.

Русский

В категории с структурой StrongEpiCategory каждый эпиморфизм является сильной эпиморфизмом.

LaTeX

$$$\\forall f:\\, P \\to Q,\\ [\\mathrm{Epi}(f)]\\Rightarrow \\mathrm{StrongEpi}(f).$$$

Lean4

theorem strongEpi_of_epi [StrongEpiCategory C] (f : P ⟶ Q) [Epi f] : StrongEpi f :=
  StrongEpiCategory.strongEpi_of_epi _

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