balanced_of_strongEpiCategory — Mathlib

English

If the category is a StrongEpiCategory, then it is Balanced; i.e., mono plus epi implies isomorphism.

Русский

Если категория является StrongEpiCategory, то она Balanced; то есть моно и эпиморфизм вместе приводят к изоморфизму.

LaTeX

$$$\\forall f:\\, X \\to Y,\\ (\\mathrm{Mono}(f) \\land \\mathrm{Epi}(f)) \\Rightarrow \\mathrm{IsIso}(f).$$$

Lean4

instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C where
  isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _

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