map_mono — Mathlib

English

If f: W → Y and g: X → Z are mono, then prod.map f g is mono (assuming HasBinaryProduct W X and HasBinaryProduct Y Z).

Русский

Если f: W → Y и g: X → Z моно, то prod.map f g моно (при условии существования бинарного произведения).

LaTeX

$$$Mono(f) \\land Mono(g) \\Rightarrow Mono( prod.map f g )$$$

Lean4

instance map_mono {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g]
    [HasBinaryProduct W X] [HasBinaryProduct Y Z] : Mono (prod.map f g) :=
  ⟨fun i₁ i₂ h => by
    ext
    · rw [← cancel_mono f]
      simpa using congr_arg (fun f => f ≫ prod.fst) h
    · rw [← cancel_mono g]
      simpa using congr_arg (fun f => f ≫ prod.snd) h⟩

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