epi_of_epi_image — Mathlib

English

If HasImage f and Epi(imageι f) and Epi(factorThruImage f) then Epi f.

Русский

Если имеется образ f, и image.ι f эпиморфизм, и factorThruImage f эпиморфизм, то f — эпиморфизм.

LaTeX

$$$ [HasImage f] \\; [Epi(image.ι f)] \\; [Epi(factorThruImage f)] \\Rightarrow Epi f $$$

Lean4

theorem epi_of_epi_image {X Y : C} (f : X ⟶ Y) [HasImage f] [Epi (image.ι f)] [Epi (factorThruImage f)] : Epi f :=
  by
  rw [← image.fac f]
  apply epi_comp

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