instIsSplitEpiComp — Mathlib

English

If f and g are split monos, then f ≫ g is a split mono.

Русский

Если f и g являются раздельными мономорфизмами, то их композиция f ≫ g является раздельным мономорфизмом.

LaTeX

$$$ \forall X,Y,Z\; (f: X \to Y) (g: Y \to Z),\; \mathrm{IsSplitMono}(f), \mathrm{IsSplitMono}(g) \Rightarrow \mathrm{IsSplitMono}(f \;\gg\; g).$$$

Lean4

instance {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitEpi f] [hg : IsSplitEpi g] : IsSplitEpi (f ≫ g) :=
  IsSplitEpi.mk' <| hf.exists_splitEpi.some.comp hg.exists_splitEpi.some

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