isIso_of_regularMono_of_epi

Mathlib.CategoryTheory.Limits.Shapes.RegularMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isIso_of_regularMono_of_epi

← MathLib Explorer

English

A regular mono that is epi implies an isomorphism.

Русский

Регулярное моно с эпиморфизмом подразумевает изоморфизм.

LaTeX

$$[RegularMono f] ∧ [Epi f] ⇒ IsIso f$$

Lean4

/-- A regular monomorphism is an isomorphism if it is an epimorphism. -/
theorem isIso_of_regularMono_of_epi (f : X ⟶ Y) [RegularMono f] [Epi f] : IsIso f :=
  isIso_of_epi_of_strongMono _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru