Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 07:39 cffa0311

View on Github →

feat(category_theory): full_of_surjective (#14974)

Estimated changes

Modified src/category_theory/functor/fully_faithful.lean

modified theorem category_theory.functor.map_injective

added theorem category_theory.functor.map_surjective