mono_lift_of_mono_left — Mathlib

English

If f: W → X is monic, then the lift map ⟨f,g⟩: W → X × Y is monic for any g: W → Y; i.e., prod.lift f g is mono whenever f is mono.

Русский

Если f: W → X моно, тогда отображение ⟨f,g⟩: W → X × Y моно для любого g: W → Y; то есть prod.lift f g моно, если f моно.

LaTeX

$$$Mono(f) \\Rightarrow Mono( prod.lift\(\n f,g\n) )$$$

Lean4

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

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