mono_lift_of_mono_left — Mathlib

English

The left injection is a split mono; it has a section given by biprod.fst.

Русский

Левое вложение является разложимой моно-инъекцией, секция задаётся biprod.fst.

LaTeX

$$$\text{Inl is split mono with section }\text{ = biprod.fst}$$$

Lean4

instance mono_lift_of_mono_left {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] :
    Mono (biprod.lift f g) :=
  mono_of_mono_fac <| biprod.lift_fst _ _

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