isoModSerre_of_mono — Mathlib

English

If f is mono and hf : P.epiModSerre f holds, then P.isoModSerre f holds.

Русский

Если f моно и выполняется P.epiModSerre f, то P.isoModSerre f.

LaTeX

$$$\forall X,Y\ f:X\to Y\,\big(\operatorname{Mono}(f) \Rightarrow (P\operatorname{epiModSerre}(f)\Rightarrow P\operatorname{isoModSerre}(f))\big)$$$

Lean4

theorem isoModSerre_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (hf : P.epiModSerre f) : P.isoModSerre f := by
  rwa [isoModSerre_iff_of_mono]

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