strongMono_of_isIso — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- An isomorphism is in particular a strong monomorphism. -/
instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f
    where
  mono := by infer_instance
  rlp {_ _} _ := HasLiftingProperty.of_right_iso _ _

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