of_mono_retraction — Mathlib

English

Every split mono whose retraction is mono is an iso.

Русский

Каждый раздельный моно, чья ретракция моно, является изоморфизмом.

LaTeX

$$$ \forall X,Y\;(f: X \to Y),\; \mathrm{SplitMono}(f) \Rightarrow [\mathrm{Mono}(\mathrm{retraction}(f))] \Rightarrow \mathrm{IsIso}(f).$$$

Lean4

/-- Every split mono whose retraction is mono is an iso. -/
theorem of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] [hf' : Mono <| retraction f] : IsIso f :=
  @IsIso.of_mono_retraction' _ _ _ _ _ hf.exists_splitMono.some hf'

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