instIsSplitMonoComp — Mathlib

English

If f: X → Y and g: Y → Z are split monos, then f ≫ g is a split mono.

Русский

Пусть f: X → Y и g: Y → Z — раздельные мономорфизмы; тогда композиция 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 : IsSplitMono f] [hg : IsSplitMono g] : IsSplitMono (f ≫ g) :=
  IsSplitMono.mk' <| hf.exists_splitMono.some.comp hg.exists_splitMono.some

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