Commit 2026-04-17 18:38 8c41661a

View on Github →

feat(CategoryTheory/MorphismProperty/Comma): add MorphismProperty.Arrow (#37540) This is needed for the category of topological pairs (#36621).

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added theorem CategoryTheory.MorphismProperty.Arrow.Hom.ext

added def CategoryTheory.MorphismProperty.Arrow.Hom.mk

added theorem CategoryTheory.MorphismProperty.Arrow.changeProp_obj_hom

added theorem CategoryTheory.MorphismProperty.Arrow.changeProp_obj_left

added theorem CategoryTheory.MorphismProperty.Arrow.changeProp_obj_right

added theorem CategoryTheory.MorphismProperty.Arrow.forget_comp_leftFunc_map

added theorem CategoryTheory.MorphismProperty.Arrow.forget_comp_rightFunc_map

added theorem CategoryTheory.MorphismProperty.Arrow.w

modified def CategoryTheory.MorphismProperty.Over.Hom.mk

modified def CategoryTheory.MorphismProperty.Under.Hom.mk