epi_comp' — Mathlib

English

The same statement as epi_comp, but with explicit epi arguments: if hf : Epi f and hg : Epi g, then Epi (f ≫ g).

Русский

То же самое, что и в epi_comp, но с явными аргументами эпиморфизма: если hf : Epi f и hg : Epi g, то Epi(f ≫ g).

LaTeX

$$$ {f:X\\to Y} {g:Y\\to Z} (hf:\\mathrm{Epi}\ f) (hg:\\mathrm{Epi}\ g) : \\mathrm{Epi}(f\\circ g)$$$

Lean4

/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as explicit arguments. For a version taking them as typeclass arguments, see `epi_comp`. -/
theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) : Epi (f ≫ g) :=
  inferInstance

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