strongEpi_comp — Mathlib

English

The composition of two strong epimorphisms is a strong epimorphism.

Русский

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

LaTeX

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

Lean4

/-- The composition of two strong epimorphisms is a strong epimorphism. -/
theorem strongEpi_comp [StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g) :=
  { epi := epi_comp _ _
    llp := by
      intros
      infer_instance }

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