epi_to — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Any morphism to an initial object is epi. -/
theorem epi_to {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : Epi f := by haveI := t.isSplitEpi_to f; infer_instance

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