strongMono_comp — Mathlib

English

The composition of two strong monomorphisms is a strong monomorphism.

Русский

Произведение двух сильных мономорфизмов является сильным мономорфизмом.

LaTeX

$$$[StrongMono f] [StrongMono g] :\; \text{StrongMono}(f \circ g)$$$

Lean4

/-- The composition of two strong monomorphisms is a strong monomorphism. -/
theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
  { mono := mono_comp _ _
    rlp := by
      intros
      infer_instance }

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