epi_of_epi_fac — Mathlib

English

Let f: X → Y, g: Y → Z, h: X → Z with h = f ∘ g and h is epi; then g is epi.

Русский

Пусть f: X → Y, g: Y → Z, h: X → Z так, что h = f ∘ g и h эпиморфизм; тогда g — эпиморфизм.

LaTeX

$$$$\\forall X,Y,Z \\; \\forall f:X\\to Y \\; \\forall g:Y\\to Z \\; \\forall h:X\\to Z,\\; [\\mathrm{Epi}\\, h],\\; f\\circ g = h \\Rightarrow \\mathrm{Epi}(g).$$$$

Lean4

theorem epi_of_epi_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Epi h] (w : f ≫ g = h) : Epi g := by subst h;
  exact epi_of_epi f g

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