strongEpi_of_isIso — Mathlib

English

If f is an isomorphism, then f is a strong epimorphism.

Русский

Если стрелка f является изоморфизмом, то она является сильной эпиморфизмом.

LaTeX

$$$\\forall \\; f,\\; \\mathrm{IsIso}(f) \\Rightarrow \\mathrm{StrongEpi}(f).$$$

Lean4

/-- An isomorphism is in particular a strong epimorphism. -/
instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f
    where
  epi := by infer_instance
  llp {_ _} _ := HasLiftingProperty.of_left_iso _ _

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