isIso_of_epi_of_strongMono — Mathlib

English

If f is epi and strong mono, then f is an isomorphism.

Русский

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

LaTeX

$$$\\forall f:\\, P \\to Q,\\ [\\mathrm{Epi}(f)]\\land [\\mathrm{StrongMono}(f)]\\Rightarrow \\mathrm{IsIso}(f).$$$

Lean4

/-- A strong monomorphism that is an epimorphism is an isomorphism. -/
theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩

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