Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.RespectsIso.mk

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  (∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) →
    (∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) → P.RespectsIso

Defined in

Mathlib.CategoryTheory.MorphismProperty.Basic

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses Classical.choice

Assumes

CategoryTheory.Category