mono_comp' — Mathlib

English

The same as mono_comp but with explicit monos: if hf : Mono f and hg : Mono g, then Mono (f ≫ g).

Русский

То же самое, что и в Mono_comp, но с явными моно: если hf : Mono f и hg : Mono g, то Mono (f ≫ g).

LaTeX

$$$ {f:X\\to Y} {g:Y\\to Z} (hf:\\mathrm{Mono}\ f) (hg:\\mathrm{Mono}\ g): \\mathrm{Mono}(f\\circ g)$$$

Lean4

/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp`.
-/
theorem mono_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Mono f) (hg : Mono g) : Mono (f ≫ g) :=
  inferInstance

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