epi_desc_of_epi_left — Mathlib

English

If f: X → W is an epimorphism, then coprod.desc f g is epi for any g: Y → W; i.e., the coproduct descent along f is an epimorphism.

Русский

Если f: X → W эпиморфизм, тогда coprod.desc f g эпиморфизм для любого g: Y → W.

LaTeX

$$$Epi(f) \\Rightarrow Epi( coprod.desc(f,g) )$$$

Lean4

instance epi_desc_of_epi_left {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] :
    Epi (coprod.desc f g) :=
  epi_of_epi_fac <| coprod.inl_desc _ _

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