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 : SplitMono f) [Mono <| hf.retraction] : IsIso f :=
  ⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id <| hf.retraction).mp (by simp)⟩⟩⟩

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