Skip to content

Commit

Permalink
made IsStableUnderComposition.unop an instance
Browse files Browse the repository at this point in the history
  • Loading branch information
@joelriou
joelriou committed Apr 28, 2024
1 parent 1491bf2 commit 70e66e2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/MorphismProperty/Composition.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ instance IsStableUnderComposition.op {P : MorphismProperty C} [P.IsStableUnderCo
comp_mem f g hf hg := P.comp_mem g.unop f.unop hg hf
#align category_theory.morphism_property.stable_under_composition.op CategoryTheory.MorphismProperty.IsStableUnderComposition.op

theorem IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] :
instance IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] :
P.unop.IsStableUnderComposition where
comp_mem f g hf hg := P.comp_mem g.op f.op hg hf
#align category_theory.morphism_property.stable_under_composition.unop CategoryTheory.MorphismProperty.IsStableUnderComposition.unop
Expand Down

0 comments on commit 70e66e2

Please sign in to comment.