mono_lift_of_mono_right — Mathlib

English

The right injection is a split mono; it has a section given by biprod.snd.

Русский

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

LaTeX

$$$\text{Inr is split mono with section }\text{ = biprod.snd}$$$

Lean4

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

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