isomorphisms_le_of_containsIdentities

English

If P contains identities and respects isomorphisms, then all isomorphisms belong to P.

Русский

Если P содержит тождественные и удовлетворяет изоморфизмам, тогда все изоморфизмы принадлежат P.

LaTeX

$$isomorphisms C ≤ P$$

Lean4

theorem isomorphisms_le_of_containsIdentities (P : MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] :
    isomorphisms C ≤ P := fun _ _ f (_ : IsIso f) ↦ P.of_isIso f

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