Commit 2022-12-29 11:25 43520f09

View on Github →

feat: port CategoryTheory.FullSubcategory (#1126)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/FullSubcategory.lean

added def CategoryTheory.FullSubcategory.lift

added def CategoryTheory.FullSubcategory.lift_comp_inclusion

added theorem CategoryTheory.FullSubcategory.lift_comp_map

added def CategoryTheory.FullSubcategory.map

added theorem CategoryTheory.FullSubcategory.map_inclusion

added structure CategoryTheory.FullSubcategory

added def CategoryTheory.InducedCategory

added theorem CategoryTheory.fullSubcategoryInclusion.map

added theorem CategoryTheory.fullSubcategoryInclusion.obj

added def CategoryTheory.fullSubcategoryInclusion

added theorem CategoryTheory.fullSubcategoryInclusion_map_lift_map

added theorem CategoryTheory.fullSubcategoryInclusion_obj_lift_obj

added def CategoryTheory.inducedFunctor