Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:40 50398e50

View on Github →

feat(category_theory/full_subcategory): induced categories

Estimated changes

Modified src/category_theory/full_subcategory.lean

added theorem category_theory.full_subcategory_inclusion.map

added theorem category_theory.full_subcategory_inclusion.obj

modified def category_theory.full_subcategory_inclusion

added def category_theory.induced_category

added theorem category_theory.induced_functor.hom

added theorem category_theory.induced_functor.obj

added def category_theory.induced_functor