mono_comp_iff_of_mono — Mathlib

English

When g is a mono, f ≫ g is mono iff f is mono.

Русский

Если g моно, то f ≫ g моно тогда и только тогда, когда f моно.

LaTeX

$$$ {X Y Z : C} (f : X \to Y) (g : Y \to Z) [\mathrm{Mono}(g)] : \mathrm{Mono}(f \gg g) \Leftrightarrow \mathrm{Mono}(f).$$$

Lean4

/-- When `g` is a monomorphism, `f ≫ g` is monic iff `f` is. -/
@[simp]
theorem mono_comp_iff_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono g] : Mono (f ≫ g) ↔ Mono f :=
  ⟨fun _ ↦ mono_of_mono _ g, fun _ ↦ inferInstance⟩

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