inr_of_epi — Mathlib

English

If HasPushout f g and Epi f, then pushout.inr is epi.

Русский

Если существует пушпокойон f,g и f эпиморфизм, то pushout.inr эпиморфизм.

LaTeX

$$$\\operatorname{Epi}(\\mathrm{pushout.inr}\\ f\\ g)$$$

Lean4

/-- The pushout of an epimorphism is an epimorphism -/
instance inr_of_epi {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] [Epi f] :
    Epi (pushout.inr _ _ : Z ⟶ pushout f g) :=
  PushoutCocone.epi_inr_of_is_pushout_of_epi (colimit.isColimit _)

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