isSplitEpi_to — Mathlib

English

Any morphism to an initial object is epi; i.e., if t is initial at X and f: Y → X, then f is an epimorphism.

Русский

Любой морфизм в начальный объект является эпиморфизмом; то есть если t начальный в X и f: Y → X, то f — эпиморфизм.

LaTeX

$$$(t:\\IsInitial X)\\ i\\ (f: Y\\to X)\\Rightarrow \\mathrm{Epi}(f)$$$

Lean4

/-- Any morphism to an initial object is split epi. -/
theorem isSplitEpi_to {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : IsSplitEpi f :=
  IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩

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