isSplitEpi_of_epi — Mathlib

English

Every split epi is epi.

Русский

Каждый раздельный эпиморфизм является эпиморфизмом.

LaTeX

$$$ \forall X,Y\,(f: X \to Y),\; \mathrm{SplitEpi}(f) \Rightarrow \mathrm{Epi}(f).$$$

Lean4

/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
    instance because it would create an instance loop. -/
theorem isSplitEpi_of_epi [SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f :=
  SplitEpiCategory.isSplitEpi_of_epi _

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