Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 16:13 e542154b

View on Github →

feat(category_theory/full_subcategory): full_subcategory.map and full_subcategory.lift (#12335)

Estimated changes

Modified src/category_theory/full_subcategory.lean

added theorem category_theory.full_subcategory.inclusion_map_lift_map

added theorem category_theory.full_subcategory.inclusion_obj_lift_obj

added def category_theory.full_subcategory.lift

added def category_theory.full_subcategory.lift_comp_inclusion

added theorem category_theory.full_subcategory.lift_comp_map

added def category_theory.full_subcategory.map

added theorem category_theory.full_subcategory.map_inclusion

Modified src/category_theory/functor/fully_faithful.lean

added def category_theory.full.of_comp_faithful_iso