of_isIso — Mathlib

English

If P is stable under composition and contains identities, then every isomorphism belongs to P.

Русский

Если P устойчиво к композиции и содержит тождества, то любая изоморфизма принадлежит P.

LaTeX

$$$\\forall X,Y\\ f:\\,X\\to Y, [IsIso f] \\Rightarrow P f$$$

Lean4

theorem of_isIso (P : MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] {X Y : C} (f : X ⟶ Y) [IsIso f] :
    P f :=
  Category.id_comp f ▸ RespectsIso.postcomp P f (𝟙 X) (P.id_mem X)

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